The Coq mailing list

[Jan-Oliver Kaiser <janno AT mpi-sws.org>]

Here's some further illustration of the problem Jacques-Henri mentioned. 
I included different variations because I had initially thought that 
maybe it could be worked around by making the FMap class or instance 
polymorphic. But it turns out that that doesn't help at all.

Now, the example I use doesn't make any sense on it's own but I am not 
convinced that one couldn't come up with more sensible ways of 
triggering universe inconsistencies in this setup.

Best,
Janno


From Coq Require Import List.

Module BuiltinLists.
  Class Fmap (G : Type -> Type) := fmap : forall A B (f : A -> B) , G A
-> G B.

  Instance list_Fmap : Fmap list := map.


  Fail Definition fails := map _ (cons list_Fmap nil). (* sad face *)
End BuiltinLists.

Module BuiltinListsPolyClass.
  Polymorphic Class Fmap (G : Type -> Type) := fmap : forall A B (f : A
-> B) , G A -> G B.

  Instance list_Fmap : Fmap list := map.

  Fail Definition fails := map _ (cons list_Fmap nil). (* sad face *)
End BuiltinListsPolyClass.


Module BuiltinListsPolyInstance.
  Polymorphic Class Fmap (G : Type -> Type) := fmap : forall A B (f : A
-> B) , G A -> G B.

  Polymorphic Instance list_Fmap : Fmap list := map.

  Fail Definition fails := map _ (cons list_Fmap nil). (* sad face *)
End BuiltinListsPolyInstance.


Module PolyLists.
  Polymorphic Inductive list {A : Type} := | nil : list | cons : A ->
list -> list.
  Arguments list A : clear implicits.
  Polymorphic Definition map {A B : Type} (f : A -> B) := fix go l :=
match l with | nil => nil | cons a l => cons (f a) (go l) end.
  Arguments map [A B].
  Polymorphic Class Fmap (G : Type -> Type) := fmap : forall A B (f : A
-> B) , G A -> G B.

  Polymorphic Instance list_Fmap : Fmap list := map.

  Definition works := map id (cons list_Fmap nil). (* works but now we 
can't use `list` from the prelude *)
End PolyLists.


On 09/06/2017 05:12 PM, Jacques-Henri Jourdan wrote:
> Le 06/09/2017 à 13:58, Jacques-Henri Jourdan a écrit :
> > Reason 1)
> >
> > Partially applying a template polymorphic type does not trigger
> > instantiation with fresh universe variables, and we do not understand
> > why. This issue has already been raised on this mailing list on Sat,
> > 22 Oct 2016 by Gregory Malecha in a post entitled "list :: nil?", but
> > I do not quite understand the answer. At that time, Matthieu answered :
> >
> >      >   Indeed, in the template case partial applications do not give
> > you a fresh instance (because there's no way to know what the fresh
> > levels are in that case, when retyping) , but an eta-expanded version
> > will work I think, e.g fun X => list X, as then we can look at the
> > type of X to determine the type of list X.
> >
> > What does "because there's no way to know what the fresh levels are in
> > that case, when retyping"?
> > Can't you just use fresh level and unify them with whatever they need
> > to be unified with, depending on the context?
> > Why is this a problem for template polymorphism and not for full
> > polymorphism?
> > Also, more fundamentally, why doesn't that break subject reduction,
> > given that eta-reduction is part of Coq's conversion rules?
>
> Maybe I should explain why this is a problem for us: It is not possible,
> in our case, to eta-expand the list type where it appears, because it
> appears as a parameter of a typeclass that needs to unify with
> non-eta-expanded instances of list.
>
> That is, we have a typeclass `FMap : (Type -> Type) -> Type`, and we
> want to define an instance of type `FMap list`. An instance of type
> `FMap (fun X => list X) would not work, because it would not be selected
> when searching for instances of type `FMap list`.