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?

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

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).

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

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.

looks like the bug lived between 74065295bc5bd66b43f4c209d4a08dc040b7bf4e and 1ae016501eb0fe3e8dfa774e682a89612f337c0f

The latter is not a commit in the Coq repo according to GitHub or my git clone.

So you probably meant 45fc3d399a13df18ee9afce7f89ca790630bf271

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?

(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.)

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...

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

instead.

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.

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.

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: Jun 20 2024 at 12:02 UTC