I have a simple question about using the specialize tactic in Coq for typeclass-based code. Specifically, I am using stdpp and I have a type lcmm_memory that is defined to be gmap nat lcmm_val.
Why doesn't the first way to instantiate the hypo H below work? Looks like the with (...:=...) syntax does not work well with typeclasses or am I missing something?
Definition comp (μ1 μ2 : lcmm_memory) :=
μ1 ∪ μ2.
Theorem foo : forall A (μ μ1 μ2 : lcmm_memory),
(forall μ, A μ) -> A (μ1 ∪ μ2).
Proof.
intros ? ? ? ? H.
(* "Cannot infer the implicit parameter
Union of union whose type is 'Union lcmm_memory'
(no type class instance found) in environment: [...]" *)
Fail (specialize H with (μ:=μ1 ∪ μ2)).
(* But this works? *)
specialize (H (μ1 ∪ μ2)).
Undo.
(* This works fine (since no typeclass lookup really here): *)
specialize H with (μ:=comp μ1 μ2).
Undo.
(* E.g. the remember tactic seems to work well with typeclasses: *)
remember (μ1 ∪ μ2) as μtmp.
specialize H with (μ:=μtmp).
subst μtmp.
(* etc. *)
assumption.
Qed.
Filed as a bug/feature request at https://github.com/coq/coq/issues/18711, so marking this question as solved.