The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT normalesup.org>]

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`.

-- 
JH

Attachment: signature.asc
Description: OpenPGP digital signature