I'm experimenting with `Hint Mode`

for typeclasses, and it seems to prevent typeclass resolution even when there are no existentials anywhere. For example, I tried adding it to `Functor`

/`Applicative`

/`Monad`

in ext-lib. However this seems to break the definition of `sequence`

in the `Traversable`

module, where the `Ap : Applicative F`

parameter is no longer inferred: https://github.com/coq-community/coq-ext-lib/commit/15a5c2f9c7c3c63782e74bce331c24bb76e1c5ef#diff-2d60d7e4e8f5aebd04eb6a6aecce320f435f73c17cb3a919cd278530b3f5d85eR16

```
(* Structures/Monad.v *)
Class Applicative@{d c} (T : Type@{d} -> Type@{c}) :=
(* ... *)
Global Hint Mode Applicative ! : typeclass_instances. (* Added this line *)
(* Structures/Traversable.v *)
Polymorphic Definition sequence@{d r}
{T : Type@{d} -> Type@{r}}
{Tr:Traversable T}
{F : Type@{d} -> Type@{r}} {Ap:Applicative F} {A : Type@{d}}
: T (F A) -> F (T A) := mapT (Ap := Ap) (@id _).
(* Ap cannot be inferred ^ *)
(* Replacing (Ap := Ap) with (Ap := _) yields an error:
The following term contains unresolved implicit arguments:
(fun (T : Type -> Type) (Tr : Traversable T) (F : Type -> Type)
(Ap : Applicative F) (A : Type) => mapT (id (A:=F A)))
More precisely:
- ?Ap: Cannot infer this placeholder of type "Applicative F" (no type class
instance found) in
environment:
T : Type -> Type
Tr : Traversable T
F : Type -> Type
Ap : Applicative F
A : Type
*)
```

What's going on?

you might be the first to use `Hint Mode`

with universe polymorphism, and there are some known bugs in the tracker even without univ-poly

It seems to persist even without universe polymorphism :/ I'll go and report that.

Actually this might be somewhat unrelated to hint mode. Here's a simpler inference problem without classes.

Why does this fail type inference? I also tried a few bidirectional (`Arguments trav _ _ &`

) annotations with no luck.

```
Definition trav : forall {T F} {A B}, (A -> F B) -> (T A -> F (T B)).
Admitted.
Definition sequence {T F} {A} (u : T (F A)) : F (T A)
:= trav (fun x => x) u. (* ERROR *)
(*
The following term contains unresolved implicit arguments:
(fun (T F : Type -> Type) (A : Type) (u : T (F A)) =>
trav (fun x : ?F ?B => x) u)
More precisely:
- ?T: Cannot infer the implicit parameter T of trav whose type is
"Type -> Type" in environment:
T, F : Type -> Type
A : Type
u : T (F A)
- ?F: Cannot infer the implicit parameter F of trav whose type is
"Type -> Type" in environment:
T, F : Type -> Type
A : Type
u : T (F A)
- ?B: Cannot infer the implicit parameter B of trav whose type is
"Type" in environment:
T, F : Type -> Type
A : Type
u : T (F A)
*)
```

this makes more sense… this code relies on higher-order unification; I think in Haskell HOU works better by relying on injectivity of type constructors.

sorry, it’s worse: Haskell doesn’t have type lambdas, which means it really does FOU.

here, one must solve ?A := ?F ?B, ?T ?A := T (F A), and ?F (?T ?B) := F (T A); in Haskell, to solve ?T ?A := T (F A), picking ?T = T and ?A = F A is a complete strategy! In Coq it isn't.

IIRC, when I looked at this problem for Scala, I ended up concluding that even pattern higher-order unification is not good enough for translating Haskell with good inference, but I don't have notes from back then. In the end, Scala (which does have lambdas) copied Haskell's algorithm as an heuristic.

to be more formal, the strategy to turn this into FOU is to treat `app`

as an _injective_ constructor.

Last updated: Sep 23 2023 at 15:01 UTC