The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi Matthieu,

ah, that's interesting!  I think I actually ran into this ~2 years ago
when working on Iris.  So, this is not something that just comes up when
doing MetaCoq.

What I wanted to do for Iris was parameterize the logic by a list of
functors (describing the ghost state that will be available).  I ran
into universe inconsistencies that we ended up fixing by having our own
copy of the list type.  The setup has since changed somewhat, but at
least the comment survived:
<https://gitlab.mpi-sws.org/FP/iris-coq/blob/f96a894b14fe7095bb5ac5b937abd31e40316858/theories/base_logic/lib/iprop.v#L37>
This development also has the problematic FMap instance.

So, this is actually a problem that one can run into doing "normal" Coq
work, not just doing Coq metaprogramming.

Thanks for digging into this, at least now we understand. :)

Kind regards,
Ralf

On 12.09.2017 20:30, Matthieu Sozeau wrote:
> Hi,
> 
>   template polymorphic inductives can't be instantiated by universes,
> one could only "refresh" their type but that would only be useful for
> the conclusion, and even then I don't know what we could do in the
> kernel, the fresh universes have no place to be recorded in the
> representation. The domain types would still have to be convertible,
> e.g. list's universe i would have to be equal to the domain of Fmap's G
> operator in the Fmap list application. Otherwise said, template
> polymorphism does not go as far as making the domain of the G type
> constructor a "parameter" of Fmap.
> Also, singleton classes like Fmap do not have template polymorphism,
> you'd need Class Fmap G := { fmap : ... } to declare an inductive
> instead of a definition, but that doesn't change the problem.
> 
> ```
>  Module BuiltinLists.
>    Universe i.
>    Class Fmap (G : Type@{i} -> Type) := fmap : forall {A B : Type@{i}}
> (f : A -> B) , G A
> -> G B.
>    Set Printing Universes.
>    Instance list_Fmap : Fmap list := map.
>    (* Forces lists' Datatypes.44 = i *)
>    Fail Definition fails := map _ (cons list_Fmap nil).
>    (* (list_Fmap : Fmap list : Type@{i+1,..) > i = Datatypes.44 *)
> End BuiltinLists.
> ```
> 
>> 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?
> 
> As mentioned by Guillaume, eta is only about conversion.
> The difference between template and full is exactly that list (and Fmap,
> and map) get universe instances attached to them in the internal
> representation, while template polymorphic inductives need their
> parameters types to typecheck (i.e. we need to see list A to infer its
> type using template polymorphism, which will depend on A's inferred
> type, partial applications don't have enough information to do that). So
> that leaves only eta-expansion to get out of your conundrum. Your
> example is even worsened by the partial application of map in list_Fmap,
> the following works:
> 
> ```
> Module BuiltinListsEtaMap.
>   Class Fmap (G : Type -> Type) := fmap : forall {A B} (f : A
> -> B) , G A -> G B.
> 
>    Instance list_Fmap : Fmap list :=
>      fun A B => @map A B.
> 
>    Definition succeeds := map id (cons list_Fmap nil). 
> (* This is because map's universes are not fixed by the list_Fmap
> implementation in this case. However fmap id fails for the reason above *)
>   Fail Definition fails := fmap id (cons list_Fmap nil). 
> End BuiltinListsEtaMap.
> ```
> 
> You could work around it a little bit using a polymorphic class and
> instance,
> but won't be able to "tie the knot" by applying fmap on lists containing
> Fmap list objects which might be what you want.
> 
> ```
> Module BuiltinListsEtaMap.
>    Universe i.
>    Polymorphic Class Fmap@{i} (G : Type@{i} -> Type@{i}) := fmap :
> forall {A B : Type@{i}} (f : A
> -> B) , G A -> G B.
> 
>   (** This ones fully polymorphic, i is only bounded by global floating
> universes which are meant to go as high as necessary *)
>   Polymorphic Instance list_Fmap@{i} : Fmap@{i} (fun A : Type@{i} =>
> list A) := 
>      fun A B => @map A B.
> 
>   (** This instance is for the fixed Datatypes.44 universe *)
>   Instance list_Fmap' : Fmap list := list_Fmap.
>   (** One can use Fmap' like this *)
>   Check (fmap S (cons 0 nil)).
>   (** One can use Fmap' like this *)
>   Check (fmap (@tl nat) nil).
>   (** But not like this, as list_Fmap' sort included the global list
> universe *)
>   Fail Definition fail' := fmap (@id _) (cons list_Fmap' nil).
> 
>   Definition succeeds := fmap id (cons list_Fmap nil).
> End BuiltinListsEtaMap.
> ```
> 
> Hope this helps,
> -- Matthieu
> 
> On Mon, Sep 11, 2017 at 11:37 AM Jan-Oliver Kaiser 
> <janno AT mpi-sws.org
> <mailto:janno AT mpi-sws.org>>
>  wrote:
> 
>     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`.
>     >
>