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

newer
Installing binary tarball fails on...

Nicolas Frisby

5 Oct 2012 5 Oct '12

5:49 p.m.

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.

Show replies by date

Richard Eisenberg

5 Oct 5 Oct

10:25 p.m.

New subject: 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:

...

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.

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Gábor Lehel

6 Oct 6 Oct

8:30 a.m.

New subject: 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 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 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:

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

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

-- Your ship was destroyed in a monadic eruption.

Nicolas Frisby

1:17 p.m.

New subject: 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 length). I'll share further technical details about the context if there's interest. Thanks again! On Sat, Oct 6, 2012 at 7:30 AM, Gábor Lehel wrote:

...

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

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

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

-- Your ship was destroyed in a monadic eruption.

Gábor Lehel

1:46 p.m.

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

On Sat, Oct 6, 2012 at 7:17 PM, Nicolas Frisby 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? You could do type family Length (l :: '[k]) :: Nat type instance Length '[] = Z type instance Length (x ': xs) = S (Length xs) class (Length l ~ n) => NLong n l instance (Length l ~ n) => NLong n l and though I didn't try it that would presumably in fact restrict the list to be that long, but I'm not sure you could use it to prove things to the typechecker (though I also don't know what you want to prove).

...

-----

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

I'll share further technical details about the context if there's interest. Thanks again!

On Sat, Oct 6, 2012 at 7:30 AM, Gábor Lehel wrote:

...
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 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 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:

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

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

-- Your ship was destroyed in a monadic eruption.

-- Your ship was destroyed in a monadic eruption.

Nicolas Frisby

7 Oct 7 Oct

12:43 a.m.

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

On Sat, Oct 6, 2012 at 12:46 PM, Gábor Lehel 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.

Nicolas Frisby

8 Oct 8 Oct

2:52 a.m.

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

On Fri, Oct 5, 2012 at 9:25 PM, Richard Eisenberg 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.

Nicolas Frisby

3:39 a.m.

New subject: 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 wrote:

...

On Fri, Oct 5, 2012 at 9:25 PM, Richard Eisenberg 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.

4607

Age (days ago)

4610

Last active (days ago)

List overview

Download

7 comments

3 participants

participants (3)

Gábor Lehel
Nicolas Frisby
Richard Eisenberg