Ryan Scott (Sep 28 2022 at 16:44): Ryan Scott (Sep 28 2022 at 16:44):I have some code which typechecks without issue in Coq 8.13.1:
Definition F : bool -> Type -> Type :=
fun b x =>
if b then x else x.
Class Inhabited (a:Type) := MkInhabited { inhabitant : a }.
Global Hint Extern 5 (Inhabited ?A) =>
(apply (@MkInhabited A); intuition (eauto with typeclass_instances inh)) : typeclass_instances.
Instance Inhabited_unit : Inhabited unit :=
MkInhabited unit tt.
Instance Inhabited_F (b : bool) (a : Type) (Ha : Inhabited a) : Inhabited (F b a) :=
MkInhabited
(F b a)
(match b with
| true => inhabitant
| false => inhabitant
end).
Definition hm : forall (p : bool -> Type), forall {Inh_p : forall (_1 : bool), Inhabited (p _1)}, p true :=
fun _ _ => inhabitant.
Definition onlyWorksOnOldCoq : unit :=
hm (fun b : bool => F b unit).
On Coq 8.14.1, however, it fails to typecheck with:
The following term contains unresolved implicit arguments:
(hm (fun b : bool => F b unit))
More precisely:
- ?Inh_p: Cannot infer the implicit parameter Inh_p
of hm whose type is
"forall _1 : bool,
Inhabited ((fun b : bool => F b unit) _1)" (no
type class instance found).
Does anyone know why this happens, and if there is a way to make this code reliably typecheck across multiple Coq versions?
Gaëtan Gilbert (Sep 28 2022 at 16:57):there may have been a bug, it works on my 8.16
Ryan Scott (Sep 28 2022 at 16:59):Hm, I see. This also works in Coq 8.15.2, now that I check.
Due to project constraints, the most recent version of Coq that I can use is 8.14, so I am still interested to know if there is some way to work around the bug in Coq 8.14 (assuming that is what is causing this).
Paolo Giarrusso (Sep 28 2022 at 17:38):one strategy:
Definition onlyWorksOnOldCoq : unit.
refine (@hm (fun b : bool => F b unit) _).
(* Now do the job of type inference by hand *)
intros. simpl. apply Inhabited_F.
Defined.
I haven't tested the actual proof of the TC obligation, that part is a strawman
Paolo Giarrusso (Sep 28 2022 at 17:40):you can also turn the result back into a term —Definition onlyWorksOnOldCoq : unit := @hm (fun b : bool => F b unit) (... manually constructed instance ...)., or write another hint extern that helps TC search.
Gaëtan Gilbert (Sep 28 2022 at 18:07):looks like the bug lived between 74065295bc5bd66b43f4c209d4a08dc040b7bf4e and 1ae016501eb0fe3e8dfa774e682a89612f337c0f
Théo Zimmermann (Sep 28 2022 at 18:14):The latter is not a commit in the Coq repo according to GitHub or my git clone.
Théo Zimmermann (Sep 28 2022 at 18:14):So you probably meant 45fc3d399a13df18ee9afce7f89ca790630bf271
Ryan Scott (Sep 28 2022 at 18:34):OK. Let me ask a slightly different question, then. The reason this code exists is because I want to use a Hint to automatically resolve Inhabited instances for most things where the implementation of the instance can easily be determined with eauto/intuition. At the same time, there are some instances that must be defined manually, such as the one for F. Is the Hint Extern approach above considered an idiomatic way to accomplish this? If not, is there a better way?
Ryan Scott (Sep 28 2022 at 18:37):(If the code above seems odd, it's because it's heavily minimized from an upstream library. I can provide any additional context on what this code is doing if that would be helpful.)
Paolo Giarrusso (Sep 28 2022 at 19:12):Using Hint Extern makes sense. Calling eauto is stranger and will likely duplicate work (in principle, leading to an exponential blowup, tho probably not here): a hint need not discharge the goal completely, it is just a step in proof search. In fact, this hint will succeed even if intuition makes no progress...
Paolo Giarrusso (Sep 28 2022 at 19:13):So ignoring inh for a moment, I'd consider intuition idtac instead.
Paolo Giarrusso (Sep 28 2022 at 19:15):Another reason is that eauto and typeclasses eauto use different engines, settings, and even unification tactics, so eauto with typeclass_instances will not behave like typeclass search.
Paolo Giarrusso (Sep 28 2022 at 19:18):I don't have a specific suggestion without looking at the code; consider this a partial answer. And of course, whether this matters for you, or is worth changing design for, depends on your usecases and problems.
Paolo Giarrusso (Sep 28 2022 at 20:29):A correction: goals left by intuition idtac won't be TC goals, but that's fixable:
Global Hint Extern 5 (Inhabited ?A) =>
apply (@MkInhabited A); intuition idtac; apply inhabitant : typeclass_instances.
hints in ihn would also likely need rephrasing.
An example of eauto vs typeclasses eauto: eauto matches hints against the goal by _syntactic_ equality, while typeclasses eauto uses a form of tactic unification — in particular, definitions can be marked as Hint Transparent or Hint Opaque in typeclass_instances. Also, if your goal is forall _1 : bool, Inhabited ((fun b : bool => F b unit) _1) (as in the example), Inhabited_F can only apply with typeclasses eauto not eauto.
Last updated: Oct 13 2024 at 01:02 UTC