Stream: Coq users

Topic: Why does Hint Mode break this definition?


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

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

view this post on Zulip Li-yao (Mar 30 2022 at 15:22):

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

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

*)

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

view this post on Zulip Paolo Giarrusso (Mar 30 2022 at 19:56):

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

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

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

view this post on Zulip 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: Feb 06 2023 at 13:03 UTC