Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Backticks and universally quantified typeclass instances

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Backticks and universally quantified typeclass instances


Chronological Thread 
  • From: Jonathan Leivent <jonikelee AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Backticks and universally quantified typeclass instances
  • Date: Thu, 10 Nov 2016 16:41:14 -0500
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f170.google.com
  • Ironport-phdr: 9a23:ZNOKjhd8KbTH+XiFrRu+rP8llGMj4u6mDksu8pMizoh2WeGdxcu/Zh7h7PlgxGXEQZ/co6odzbGH6Oa4AidZvcvJmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanb75/KBu7oR/NusQYjoduN6k8xxvUqXZUZupawn9lK0iOlBjm/Mew+5Bj8yVUu/0/8sNLTLv3caclQ7FGFToqK2866tHluhnFVguP+2ATUn4KnRpSAgjK9w/1U5HsuSbnrOV92S2aPcrrTbAoXDmp8qlmRAP0hCoBKjU09nzchM5tg6JBuB+vugJxw4DUbo+WOvRxcKzSctEGSmRORctRSy5MD5mgY4cTAecMPeBVpJT9qVsUqhu+ABGhCufoyj9OnHD2wa063P4nEQrb2gIvAdMOsGrKo9XzKKcZTOe4zKvPzTXFbvNW2iny6IzWfR8/uvyMUrdwftDQyUkrDQ/KklKQqYn8Mj6Ty+8DsHCb4vJ+We6zj2MrsQJ8rzi1yssyl4XEh5gZxk3G+Cll2Io4J8C0RFRlbdOqH5ZcrTyWOoVqTs84XW1ltiQ3x7sbspChZicK0o4oxxvHZvyHbYeI5hXjWf6UIThihXJlfKuzhw+u8US80+H8WNS43VRWoiZfndnMsXcN1xPX6seZUPdy4kCh2TOX2wDS7OFLP1w0mLLFJ5I9xrM8jJkevETZEiPohUn7jbWaelgm9+S08+jnZ6/ppp6YN496kAH+NaEul9S9AeQ/NAgOXmub9vq41LL940L0W7pKjvgsnanYtJDWP9gUpqm8AwNNyIYs9w6/Dyu60NQfhXQIMFVFeAueg4f1P1HOPev3AOykg1WslTdr3+rJMqfgApXLNHjDka3ucaxz605Gm0IPyoVU4IsRAbUcKtryXFXwvZrWFEwXKQuxlsTgDtxh1ooYEUaCA7GUNr+a5V2P4OMsLu2BaacavT/8L74u4Pu43ixxokMUYaT8hchfU3u/BPkze0g=

Now I am very confused, as what you said works:

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

Variable A : Type.
Context `{tcB A}.

fails for me in both 8.5pl3 and 8.6. I have to do this to make it work:

Class tcA (X: nat).
Class tcB (X: nat) `{tcA X}.

Variable A : nat.
Context `{tcA A}.
Context `{@tcB A _}.

So, this is not merely a problem with type families.


I find it very strange that this works:

Class tcA (X: nat).
Class tcB (X: nat) `{tcA X}.

Variable A : nat.
Context `{tcA A}.
Context {x : tcB A}.

but adding a backquote ` to the last Context line fails.

-- Jonathan



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





Archive powered by MHonArc 2.6.18.

Top of Page