The Coq mailing list

[Dan Frumin <dfrumin AT cs.ru.nl>]

Dear *,

I ran into the following problem recently. Suppose I have typeclasses
(tcA T) and (tcB T) for (T : Type), whereby the second typeclass
depends on the first one.

   Class tcA (T: Type).
   Class tcB (T: Type) `{tcA T}.


If I have a [Parameter]/[Variable]
(A : Type) then I can write

  Context `{tcB A}.

and the backtick magic will register both instances for [tcB A] and
[tcA A]. However, if I have a type family T, and I want to assert [tcB
(T A)] for all types A, I run into a problem.

   Variable T : Type -> Type.
   Context `{forall A, (tcB (T A))}.

> Error: Cannot infer the implicit parameter H of tcB whose type is 
> "tcA (T A)" (no type class instance found) in environment:
> A : Type

It makes sense that it doesn't work, but does anyone know of a
workaround for this?

Kind regards,
- Dan