The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Is this what you want?:

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

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

or this?:

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

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


-- Jonathan


On 11/10/2016 09:53 AM, Dan Frumin wrote:
> 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