Stream: Coq users

Topic: Code typechecks in Coq 8.13, but not in 8.14


view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Sep 28 2022 at 16:57):

there may have been a bug, it works on my 8.16

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Sep 28 2022 at 17:39):

I haven't tested the actual proof of the TC obligation, that part is a strawman

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Sep 28 2022 at 18:07):

looks like the bug lived between 74065295bc5bd66b43f4c209d4a08dc040b7bf4e and 1ae016501eb0fe3e8dfa774e682a89612f337c0f

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Sep 28 2022 at 18:14):

So you probably meant 45fc3d399a13df18ee9afce7f89ca790630bf271

view this post on Zulip 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?

view this post on Zulip 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.)

view this post on Zulip 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...

view this post on Zulip Paolo Giarrusso (Sep 28 2022 at 19:13):

So ignoring inh for a moment, I'd consider intuition idtac instead.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: Feb 04 2023 at 21:02 UTC