Closed Type Families: type checking dumbness? [was: separate instance groups]

newer
Re: [Haskell-cafe] The evil GADTs...

older
Closed Type Families: separate...

AntC

6 Jun 2015 6 Jun '15

2:04 a.m.

...

From: AntC Date: 2015-06-04 22:39:25 GMT

Take the standard example for partial overlaps. Suppose I have a class: ...

...

I'm also getting (in more complex examples) GHC complaining it can't infer the types for the result of f. So now I'm having to put type equality constraints on the class instances, to assure it that F comes up with the right type.

In a reduced example, I'm still getting poor type checking. This is GHC 7.8.3. This seems so dumb, I'm suspecting a defect, It's similar to but much more glaring than: https://ghc.haskell.org/trac/ghc/ticket/10227 https://ghc.haskell.org/trac/ghc/ticket/9918 {-# LANGUAGE TypeFamilies, FlexibleInstances #-} module ClosedTypeFamily where data Foo b c = Foo b c deriving (Eq, Read, Show) type family F a where F (Foo Int c) = Int -- Foo Int is first instance F (Foo b Char) = Char class C a where f :: a -> F a instance C (Foo Int c) where -- compiles OK f (Foo x _) = x instance (F (Foo b Char) ~ Char) => C (Foo b Char) where f (Foo _ y) = y needs the eq constraint. Without it, GHC complains: Couldn't match expected type ‘F (Foo b Char)’ with actual type ‘Char’ Relevant bindings include f :: Foo b Char -> F (Foo b Char) In the expression: y In an equation for ‘f’: f (Foo _ y) = y Note that if I change the sequence of the family instances for F, then GHC instead complains about the class instance for (Foo Int c). OK these are overlapping class instances. But GHC's usual behaviour (without closed type families) is to postpone complaining until and unless a usage (Foo Int Char) actually turns up. BTW if I put a first family instance F (Foo Int Char) = Int to explicitly catch the overlap, then GHC complains about **both** class instances. Reminder [to Richard] I need not only types but also terms. AntC

Show replies by date

Richard Eisenberg

7 Jun 7 Jun

7:27 a.m.

This is all expected behavior. GHC's lazy overlap checking for class instances simply cannot apply to type families -- it would be unsound. I'm afraid I don't see what can be improved here. Richard On Jun 6, 2015, at 2:04 AM, AntC wrote:

...

...
From: AntC Date: 2015-06-04 22:39:25 GMT

Take the standard example for partial overlaps. Suppose I have a class: ...

...
I'm also getting (in more complex examples) GHC complaining it can't infer the types for the result of f. So now I'm having to put type equality constraints on the class instances, to assure it that F comes up with the right type.

In a reduced example, I'm still getting poor type checking. This is GHC 7.8.3. This seems so dumb, I'm suspecting a defect, It's similar to but much more glaring than: https://ghc.haskell.org/trac/ghc/ticket/10227 https://ghc.haskell.org/trac/ghc/ticket/9918

{-# LANGUAGE TypeFamilies, FlexibleInstances #-} module ClosedTypeFamily where

data Foo b c = Foo b c deriving (Eq, Read, Show)

type family F a where F (Foo Int c) = Int -- Foo Int is first instance F (Foo b Char) = Char

class C a where f :: a -> F a

instance C (Foo Int c) where -- compiles OK f (Foo x _) = x

instance (F (Foo b Char) ~ Char) => C (Foo b Char) where f (Foo _ y) = y

needs the eq constraint. Without it, GHC complains: Couldn't match expected type ‘F (Foo b Char)’ with actual type ‘Char’ Relevant bindings include f :: Foo b Char -> F (Foo b Char) In the expression: y In an equation for ‘f’: f (Foo _ y) = y

Note that if I change the sequence of the family instances for F, then GHC instead complains about the class instance for (Foo Int c).

OK these are overlapping class instances. But GHC's usual behaviour (without closed type families) is to postpone complaining until and unless a usage (Foo Int Char) actually turns up.

BTW if I put a first family instance F (Foo Int Char) = Int to explicitly catch the overlap, then GHC complains about **both** class instances.

Reminder [to Richard] I need not only types but also terms.

AntC _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Dan Doel

11:12 a.m.

It seems to me the problem is that there's no way to define classes by consecutive cases to match the family definitions. I don't know what a good syntax for that would be, since 'where' syntax is taken for those. But it seems like it would correspond fill the hole here. On Sun, Jun 7, 2015 at 7:27 AM, Richard Eisenberg wrote:

...

This is all expected behavior. GHC's lazy overlap checking for class instances simply cannot apply to type families -- it would be unsound. I'm afraid I don't see what can be improved here.

Richard

On Jun 6, 2015, at 2:04 AM, AntC wrote:

...
...
From: AntC Date: 2015-06-04 22:39:25 GMT

Take the standard example for partial overlaps. Suppose I have a class: ...

...
I'm also getting (in more complex examples) GHC complaining it can't infer the types for the result of f. So now I'm having to put type equality constraints on the class instances, to assure it that F comes up with the right type.

In a reduced example, I'm still getting poor type checking. This is GHC 7.8.3. This seems so dumb, I'm suspecting a defect, It's similar to but much more glaring than: https://ghc.haskell.org/trac/ghc/ticket/10227 https://ghc.haskell.org/trac/ghc/ticket/9918

{-# LANGUAGE TypeFamilies, FlexibleInstances #-} module ClosedTypeFamily where

data Foo b c = Foo b c deriving (Eq, Read, Show)

type family F a where F (Foo Int c) = Int -- Foo Int is first instance F (Foo b Char) = Char

class C a where f :: a -> F a

instance C (Foo Int c) where -- compiles OK f (Foo x _) = x

instance (F (Foo b Char) ~ Char) => C (Foo b Char) where f (Foo _ y) = y

needs the eq constraint. Without it, GHC complains: Couldn't match expected type ‘F (Foo b Char)’ with actual type ‘Char’ Relevant bindings include f :: Foo b Char -> F (Foo b Char) In the expression: y In an equation for ‘f’: f (Foo _ y) = y

Note that if I change the sequence of the family instances for F, then GHC instead complains about the class instance for (Foo Int c).

OK these are overlapping class instances. But GHC's usual behaviour (without closed type families) is to postpone complaining until and unless a usage (Foo Int Char) actually turns up.

BTW if I put a first family instance F (Foo Int Char) = Int to explicitly catch the overlap, then GHC complains about **both** class instances.

Reminder [to Richard] I need not only types but also terms.

AntC _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

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

adam vogt

12:36 p.m.

Hi, AntC's f can be done without -XOverlappingInstances < http://lpaste.net/7559485273839501312>, using the trick didn't work in #9918. I'm not sure extra syntax is justified to clean up this rare case. Regards, Adam On Sun, Jun 7, 2015 at 11:12 AM, Dan Doel wrote:

...

It seems to me the problem is that there's no way to define classes by consecutive cases to match the family definitions. I don't know what a good syntax for that would be, since 'where' syntax is taken for those. But it seems like it would correspond fill the hole here.

On Sun, Jun 7, 2015 at 7:27 AM, Richard Eisenberg wrote:

...
This is all expected behavior. GHC's lazy overlap checking for class instances simply cannot apply to type families -- it would be unsound. I'm afraid I don't see what can be improved here.

Richard

On Jun 6, 2015, at 2:04 AM, AntC wrote:

...
...
From: AntC Date: 2015-06-04 22:39:25 GMT

Take the standard example for partial overlaps. Suppose I have a class: ...

...
I'm also getting (in more complex examples) GHC complaining it can't infer the types for the result of f. So now I'm having to put type equality constraints on the class instances, to assure it that F comes up with the right type.

In a reduced example, I'm still getting poor type checking. This is GHC 7.8.3. This seems so dumb, I'm suspecting a defect, It's similar to but much more glaring than: https://ghc.haskell.org/trac/ghc/ticket/10227 https://ghc.haskell.org/trac/ghc/ticket/9918

{-# LANGUAGE TypeFamilies, FlexibleInstances #-} module ClosedTypeFamily where

data Foo b c = Foo b c deriving (Eq, Read, Show)

type family F a where F (Foo Int c) = Int -- Foo Int is first instance F (Foo b Char) = Char

class C a where f :: a -> F a

instance C (Foo Int c) where -- compiles OK f (Foo x _) = x

instance (F (Foo b Char) ~ Char) => C (Foo b Char) where f (Foo _ y) = y

needs the eq constraint. Without it, GHC complains: Couldn't match expected type ‘F (Foo b Char)’ with actual type ‘Char’ Relevant bindings include f :: Foo b Char -> F (Foo b Char) In the expression: y In an equation for ‘f’: f (Foo _ y) = y

Note that if I change the sequence of the family instances for F, then GHC instead complains about the class instance for (Foo Int c).

OK these are overlapping class instances. But GHC's usual behaviour (without closed type families) is to postpone complaining until and unless a usage (Foo Int Char) actually turns up.

BTW if I put a first family instance F (Foo Int Char) = Int to explicitly catch the overlap, then GHC complains about **both** class instances.

Reminder [to Richard] I need not only types but also terms.

AntC _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

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

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

Richard Eisenberg

2:36 p.m.

That's right. You're suggesting instance chains [1][2]. [1]: https://ghc.haskell.org/trac/ghc/ticket/9334 [2]: http://web.cecs.pdx.edu/~mpj/pubs/instancechains.pdf Richard On Jun 7, 2015, at 11:12 AM, Dan Doel wrote:

...

It seems to me the problem is that there's no way to define classes by consecutive cases to match the family definitions. I don't know what a good syntax for that would be, since 'where' syntax is taken for those. But it seems like it would correspond fill the hole here.

On Sun, Jun 7, 2015 at 7:27 AM, Richard Eisenberg wrote: This is all expected behavior. GHC's lazy overlap checking for class instances simply cannot apply to type families -- it would be unsound. I'm afraid I don't see what can be improved here.

Richard

On Jun 6, 2015, at 2:04 AM, AntC wrote:

...
...
From: AntC Date: 2015-06-04 22:39:25 GMT

Take the standard example for partial overlaps. Suppose I have a class: ...

...
I'm also getting (in more complex examples) GHC complaining it can't infer the types for the result of f. So now I'm having to put type equality constraints on the class instances, to assure it that F comes up with the right type.

In a reduced example, I'm still getting poor type checking. This is GHC 7.8.3. This seems so dumb, I'm suspecting a defect, It's similar to but much more glaring than: https://ghc.haskell.org/trac/ghc/ticket/10227 https://ghc.haskell.org/trac/ghc/ticket/9918

{-# LANGUAGE TypeFamilies, FlexibleInstances #-} module ClosedTypeFamily where

data Foo b c = Foo b c deriving (Eq, Read, Show)

type family F a where F (Foo Int c) = Int -- Foo Int is first instance F (Foo b Char) = Char

class C a where f :: a -> F a

instance C (Foo Int c) where -- compiles OK f (Foo x _) = x

instance (F (Foo b Char) ~ Char) => C (Foo b Char) where f (Foo _ y) = y

needs the eq constraint. Without it, GHC complains: Couldn't match expected type ‘F (Foo b Char)’ with actual type ‘Char’ Relevant bindings include f :: Foo b Char -> F (Foo b Char) In the expression: y In an equation for ‘f’: f (Foo _ y) = y

Note that if I change the sequence of the family instances for F, then GHC instead complains about the class instance for (Foo Int c).

OK these are overlapping class instances. But GHC's usual behaviour (without closed type families) is to postpone complaining until and unless a usage (Foo Int Char) actually turns up.

BTW if I put a first family instance F (Foo Int Char) = Int to explicitly catch the overlap, then GHC complains about **both** class instances.

Reminder [to Richard] I need not only types but also terms.

AntC _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

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

AntC

8 Jun 8 Jun

6:03 a.m.

...

Dan Doel writes:

It seems to me the problem is that there's no way to define classes by consecutive cases to match the family definitions.

Thanks Dan, yes we've an impedance mis-match. Closed logic for type families; Open (or Distributed) logic for class instances. I see two possible fixes: 1. Closed logic for class instances

...

I don't know what a good syntax for that would be, since 'where' syntax is taken for those.

Indeed. We could follow SQL and use 'HAVING' ;-) 2. Open/Distributed logic for type families (and class instances). Take the example type family:

...

...
type family F a where F (Foo Int c) = Int F (Foo b Char) = Char

For instance selection to move confidently from the first to the second equation, it must satisfy itself that Foo's first arg could not possibly be Int. ie (b /~ Int) Let's expose the compiler's internal workings into the surface lang. And annotate that on the second equation as F (Foo b Char) | (b /~ Int) = Char This mirrors the syntax for pattern guards. Now no usage site could ever match both equations. (And we can prove that as we validate each instance.) So we could 'float' the type instances away to appear with the class instances -- even as Associated types. (And we'd need type disequality guards on the class instances.) AntC

AntC

5:49 a.m.

...

Richard Eisenberg writes:

This is all expected behavior. ...

Thank you Richard. So to be clear what it is that's expected: For any class with overlapping instances that calls on a Closed Type Family, for all [**] instances, expect to put a type equality constraint, whose LHS is exactly the instance head, and whose RHS is exactly the RHS of the corresponding type family equation. IOW expect the type equation to appear twice (with `=` changed to `~`, modulo alpha renaming). Note [**] not quite all instances. The instance whose head is the first family equation can have the constraint omitted.

...

GHC's lazy overlap checking for class instances ...

Hmm? I don't think it's the lazy checking of whether overlapping instances apply at a use site. I think it's the eager checking at the instance declaration.

...

... I'm afraid I don't see what can be improved here.

Two suggestions: 1. Automatically generate the type eq constraint. (Or at least suggest that as a Possible fix in the error message.) 2. Don't bother with a type family in such cases. Instead use Overlaps with FunDeps. (And needs UndecidableInstances.)

...

...
On Jun 6, 2015, at 2:04 AM, AntC wrote: needs the eq constraint. Without it, GHC complains: Couldn't match expected type ‘F (Foo b Char)’ with actual type ‘Char’ Relevant bindings include f :: Foo b Char -> F (Foo b Char) In the expression: y In an equation for ‘f’: f (Foo _ y) = y

3634

Age (days ago)

3636

Last active (days ago)

List overview

Download

6 comments

4 participants

participants (4)

adam vogt
AntC
Dan Doel
Richard Eisenberg