headers
Nicolas Frisby | 5 Oct 2012 23:49
Picon
Gravatar

seemingly inconsistent behavior for "kind-indexed" type constraints in GHC 7.6

GHC 7.6 is rejecting some programs that I think ought to be well-typed.

Details here https://gist.github.com/3842579

I find this behavior particularly odd because I can get GHC to deduce
the type equalities in some contexts but not in others. In particular,
it does not deduce them inside of type class instances.

Is this a known issue? I'll create a Trac ticket if that's appropriate.

Thanks for your time.
Permalink | Reply |
headers
Richard Eisenberg | 6 Oct 2012 04:25
Favicon
Gravatar

Re: seemingly inconsistent behavior for "kind-indexed" type constraints in GHC 7.6

Hi Nick,

Interesting example.

I think GHC is right in rejecting your instance, but perhaps not for the reasons you expect.

It would be possible to add another instance to NUnits:
instance NUnits Z '[()]
This would require OverlappingInstances, but because of the possibility of further instances, GHC
rightly does not assume that a matching instance is the only possible matching instance. So, without that
assumption, there is no reason GHC should unify ts with '[].

For similar reasons, GHC does not bring the constraints on an instance into the context when an instance
matches. So, even if GHC did select the instance you want, it would not bring ('[] ~ ps) into the context.

To me, both of these problems have solutions: introduce a functional dependency on NUnits, n -> ts; and
declare the wanted instance to be "instance NUnits Z '[]", without the equality constraint. What's
interesting is that doing both of these changes didn't get the instance accepted. This *might* be a bug in
GHC, but I'd love another opinion before filing, because I'm really not sure.

Another issue at work here is that GHCi, by default, does not enable PolyKinds, even when it has loaded a file
with PolyKinds. The effect of this is that printing out polymorphic kinds will see all type variables
default to * without :set -XPolyKinds. That may have had a role to play in the commentary in the file, but I'm
not sure.

Thanks for posting!
Richard

On Oct 5, 2012, at 5:49 PM, Nicolas Frisby wrote:
(Continue reading)

Permalink | Reply |
headers
Gábor Lehel | 6 Oct 2012 14:30
Picon

Re: seemingly inconsistent behavior for "kind-indexed" type constraints in GHC 7.6

I made a version using an associated type and that seems to work fine:

https://gist.github.com/3844758

(In fact you probably don't need a class at all and a simple type
family would be enough.)

On Sat, Oct 6, 2012 at 4:25 AM, Richard Eisenberg <eir <at> cis.upenn.edu> wrote:
> Hi Nick,
>
> Interesting example.
>
> I think GHC is right in rejecting your instance, but perhaps not for the reasons you expect.
>
> It would be possible to add another instance to NUnits:
> instance NUnits Z '[()]
> This would require OverlappingInstances, but because of the possibility of further instances, GHC
rightly does not assume that a matching instance is the only possible matching instance. So, without that
assumption, there is no reason GHC should unify ts with '[].
>
> For similar reasons, GHC does not bring the constraints on an instance into the context when an instance
matches. So, even if GHC did select the instance you want, it would not bring ('[] ~ ps) into the context.
>
> To me, both of these problems have solutions: introduce a functional dependency on NUnits, n -> ts; and
declare the wanted instance to be "instance NUnits Z '[]", without the equality constraint. What's
interesting is that doing both of these changes didn't get the instance accepted. This *might* be a bug in
GHC, but I'd love another opinion before filing, because I'm really not sure.
>
> Another issue at work here is that GHCi, by default, does not enable PolyKinds, even when it has loaded a
file with PolyKinds. The effect of this is that printing out polymorphic kinds will see all type variables
(Continue reading)

Permalink | Reply |
headers
Nicolas Frisby | 6 Oct 2012 19:17
Picon
Gravatar

Re: seemingly inconsistent behavior for "kind-indexed" type constraints in GHC 7.6

Thanks. I'll have to spend some more time thinking through those, but
here's two quick responses.

1) Richard: I thought that because OverlappingInstances was not
specified (in this module or any others), GHC would commit to the
instance. If this behavior you suspect is the case, has there been a
discussion of a flag that would disable it?

2) I think I should leak some more of the details of my actual
situation; they seem important if people want to attempt work arounds
(thanks Gábor).

As you may have guessed, I'm not actually interested in a list of ()s.
My actual class is as follows.

> class NLong (n :: Nat) (ts :: [k])
>
> instance ('[] ~ ps) => NLong Z ps
> instance ((t ': pstail) ~ ps, NLong n pstail) => NLong (S n) ps

I just want to require that the list has n many elements, without
restricting those elements. This is why I'm not using fundeps and type
families — I need to be polymorphic in the elements.

Any alternative ideas given this extra specification details?

-----

Further context: I suspect that my use case for this machinery would
be supplanted if we could promote GADTs (esp. vectors of a fixed
(Continue reading)

Permalink | Reply |
headers
Gábor Lehel | 6 Oct 2012 19:46
Picon

Re: seemingly inconsistent behavior for "kind-indexed" type constraints in GHC 7.6

On Sat, Oct 6, 2012 at 7:17 PM, Nicolas Frisby <nicolas.frisby <at> gmail.com> wrote:
> Thanks. I'll have to spend some more time thinking through those, but
> here's two quick responses.
>
> 1) Richard: I thought that because OverlappingInstances was not
> specified (in this module or any others), GHC would commit to the
> instance. If this behavior you suspect is the case, has there been a
> discussion of a flag that would disable it?
>
> 2) I think I should leak some more of the details of my actual
> situation; they seem important if people want to attempt work arounds
> (thanks Gábor).
>
> As you may have guessed, I'm not actually interested in a list of ()s.
> My actual class is as follows.
>
>> class NLong (n :: Nat) (ts :: [k])
>>
>> instance ('[] ~ ps) => NLong Z ps
>> instance ((t ': pstail) ~ ps, NLong n pstail) => NLong (S n) ps
>
> I just want to require that the list has n many elements, without
> restricting those elements. This is why I'm not using fundeps and type
> families — I need to be polymorphic in the elements.
>
> Any alternative ideas given this extra specification details?

What do you use NLong for? I.e. where and how are you taking advantage
of the knowledge that the list is N long?
(Continue reading)

Permalink | Reply |
headers
Nicolas Frisby | 7 Oct 2012 06:43
Picon
Gravatar

Re: seemingly inconsistent behavior for "kind-indexed" type constraints in GHC 7.6

On Sat, Oct 6, 2012 at 12:46 PM, Gábor Lehel <illissius <at> gmail.com> wrote:
> What do you use NLong for? I.e. where and how are you taking advantage
> of the knowledge that the list is N long?

OK, some context. I'm experimenting with an augmentation of the
generic-deriving generic programming approach.

  https://github.com/nfrisby/polyvariadic-generic-deriving

Regarding the part of the library that doesn't suffer from the issue
in my original email in this thread, user code using the library
results in more accurate inferred types because of the NLong
constraints. These more accurate inferred types ultimately avoid some
"ambiguous type variable" errors in the user's code.

This new gist https://gist.github.com/3847097 demonstrates the
benefits that I get from NLong; it gives an example of it eliminating
an otherwise ambiguous type variable. It also explains the context of
the library a bit more.

Thanks.
Permalink | Reply |
headers
Nicolas Frisby | 8 Oct 2012 08:52
Picon
Gravatar

Re: seemingly inconsistent behavior for "kind-indexed" type constraints in GHC 7.6

On Fri, Oct 5, 2012 at 9:25 PM, Richard Eisenberg <eir <at> cis.upenn.edu> wrote:
> For similar reasons, GHC does not bring the constraints on an instance into the context when an instance
matches. So, even if GHC did select the instance you want, it would not bring ('[] ~ ps) into the context.

Ah, of course. I was naively letting myself regarding NLong by its
semantics and not by its instances. Silly mistake.

Part of the reason I made that mistake is that NLong is having the
desired effect on my program in other situations (as my second gist
demonstrates). I still need to characterize how that's working for me
there, but I'm sure your clarification here will surely guide me when
doing so. Thank you.

In past situations like this one, I have effected the desired
implication (to the instance context as instead of to the superclass)
via a coercion, which I make into a rank2 method of the class. It's
just rather tricky to express the type of the coercion in this case,
because of the involved Nat. I'm working on it now.
Permalink | Reply |
headers
Nicolas Frisby | 8 Oct 2012 09:39
Picon
Gravatar

Re: seemingly inconsistent behavior for "kind-indexed" type constraints in GHC 7.6

Just in case anyone is following along at home, here's what I'm going with.

> type TakeN n ts = TakeNDropM n Z ts
>
> type family TakeNDropM (n :: Nat) (which :: Nat) (ts :: [k]) :: [k]
> type instance TakeNDropM Z     which ts = '[]
> type instance TakeNDropM (S n) which ts = Nth which ts ': TakeNDropM n (S which) ts
>
> class (ts ~ TakeN n ts) => NLong (n :: Nat) (ts :: [k])

(Turns out the coercion method itself is unnecessary in this case.)

Now I just have to "prove" it (by using the requisite ~ constraints on
ts) via instances… in the morning. I think this solution will work out
nicely, based on my previous experiences.

It may turn out to be interesting to compare this convention (of
sprinkling NLong constraints everywhere) to the intended behavior of
using a promoted vector GADT for the kind of ts — eg (ts :: Vec n k).

Thanks for the help, Richard and Gábor. To everyone else, sorry for
the noise/HTH in the future.

On Mon, Oct 8, 2012 at 1:52 AM, Nicolas Frisby <nicolas.frisby <at> gmail.com> wrote:
> On Fri, Oct 5, 2012 at 9:25 PM, Richard Eisenberg <eir <at> cis.upenn.edu> wrote:
>> For similar reasons, GHC does not bring the constraints on an instance into the context when an instance
matches. So, even if GHC did select the instance you want, it would not bring ('[] ~ ps) into the context.
>
> Ah, of course. I was naively letting myself regarding NLong by its
> semantics and not by its instances. Silly mistake.
(Continue reading)

Permalink | Reply |

Gmane