The Coq mailing list

[Merlin Göttlinger <megoettlinger AT gmail.com>]

Hi,

I'm trying to "derive" typeclass instances from existing tpeclass instances by functoriality of the typeclasses.

So given a instance (ta : TC A) that is covariant in A and a function (f : A -> B) I would like to write something like (fmap f ta : TC B).

Depending on the shape of the typeclass it might also be contravariant or more likely invariant requiring two functions (ab : A -> B) (ba : B ->A).

To generalise this I wrote a typeclass Invariant (encoded with the CPS trick discussed recently). Implementing the instances of this has one issue however:

Class BPL m := { 

  verum : m;

  falsum : m;

  prop : atom -> m;

  nomi : nom -> m;

  conj : m -> m -> m;

  disj : m -> m -> m;

}.

Global Instance bpl_invar : Invariant (F := BPL) := fun r f => f {| imap__ A B := fun ab ba fa =>

        {| verum := ab verum;                                                           falsum := ab falsum;

           prop p := ab (prop p);

           nomi n := ab (nomi n);

           conj a b := ab (conj (ba a) (ba b));

           disj a b := ab (disj (ba a) (ba b))

         |}

|}.

This leaves me with a wrong type for fa resulting in a missing Instance.

A : Type

B : Type

ab : A -> B

ba : B -> A

fa : (fun B : Type => BPL B) A

?BPL : "BPL A"

if you wrap the inner record creation in let _ : BPL A := fa in ... it works as expected.

Why isn't the type of fa reduced without this wrapper? 

Is there a better way to do what I want to do?

Cheers,

Merlin