coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Backticks and universally quantified typeclass instances, Dan Frumin, 11/10/2016
- Re: [Coq-Club] Backticks and universally quantified typeclass instances, Jonathan Leivent, 11/10/2016
- Re: [Coq-Club] Backticks and universally quantified typeclass instances, Dan Frumin, 11/10/2016
- Re: [Coq-Club] Backticks and universally quantified typeclass instances, Jonathan Leivent, 11/10/2016
- Re: [Coq-Club] Backticks and universally quantified typeclass instances, Dan Frumin, 11/10/2016
- Re: [Coq-Club] Backticks and universally quantified typeclass instances, Jonathan Leivent, 11/10/2016
Archive powered by MHonArc 2.6.18.