The Coq mailing list

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

Dear Jonathan,

On 11/10, Jonathan Leivent wrote:
> 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)}}.

I don't really care about specific instances, so both snippets are
fine with me. The problem is that in my actual code, as opposed to
this small example, the second type class depends on 6 other
typeclasses, each one of those typeclasses may depend on a couple of
other typeclasses, thus resulting in a lot of boilerplate code.

I was wondering if there is a known way to circumvent such situations.

- Dan
> -- 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