Stream: Coq users

Topic: Why does Hint Mode break this definition?

Li-yao (Mar 22 2022 at 00:08):

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?

Paolo Giarrusso (Mar 30 2022 at 02:52):

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

Li-yao (Mar 30 2022 at 15:22):

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

Li-yao (Mar 30 2022 at 15:38):

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)

*)

Paolo Giarrusso (Mar 30 2022 at 19:52):

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.

Paolo Giarrusso (Mar 30 2022 at 19:56):

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

Paolo Giarrusso (Mar 30 2022 at 19:57):

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.

Paolo Giarrusso (Mar 30 2022 at 19:59):

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.

Paolo Giarrusso (Mar 30 2022 at 19:59):

to be more formal, the strategy to turn this into FOU is to treat app as an _injective_ constructor.

Last updated: Apr 19 2024 at 22:01 UTC