Opened 9 years ago

Closed 8 years ago

Last modified 7 years ago

#1968 closed bug (fixed)

data family + GADT: not implemented yet

Reported by: Remi Owned by: chak
Priority: normal Milestone: 6.10 branch
Component: Compiler (Type checker) Version: 6.9
Keywords: data type family GADT choose_univs Cc: rturk@…, tora@…, g9ks157k@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

My very first attempt at playing with data type families + GADTs went wrong, using 6.9.20071209:

{-# LANGUAGE TypeFamilies, GADTs #-}

data family HiThere a :: *

data instance HiThere () where
    HiThere :: HiThere ()
GHCi, version 6.9.20071209: http://www.haskell.org/ghc/  :? for help
Loading package base ... linking ... done.
[1 of 1] Compiling Main             ( bar.hs, interpreted )
*** Exception: typecheck/TcTyClsDecls.lhs:(878,4)-(884,42): Non-exhaustive patterns in function choose_univs

Change History (18)

comment:1 Changed 9 years ago by chak

Owner: set to chak
Summary: data family + GADT = Non-exhaustive patterns in function choose_univsdata family + GADT: not implemented yet

GADT syntax for data families is not supported yet, I would have expected a better error message, though. In your example, there is actually no need to use GADT syntax, just write

data family HiThere a :: *
data instance HiThere () = HiThere

and you should be fine.

comment:2 Changed 9 years ago by chak

Architecture: UnknownMultiple
difficulty: UnknownModerate (1 day)
Milestone: 6.10 branch
Operating System: UnknownMultiple

comment:3 Changed 9 years ago by guest

Cc: tora@… added

Also interested in this. Will the implementation allow varying non-instance types?

{-# LANGUAGE TypeFamilies, KindSignatures, GADTs #-}
module Foo2 where

data family Blah x :: * -> *

data instance Blah Bool where
  Bool1 :: Blah Bool Int
  Bool2 :: Blah Bool Char

data instance Blah Char where
  Char1 :: Blah Char Int
  Char2 :: Blah Char Char
>ghc-6.9.20080401 -c Foo2.hs 
ghc-6.9.20080401: panic! (the 'impossible' happened)
  (GHC version 6.9.20080401 for x86_64-unknown-linux):
	typecheck/TcTyClsDecls.lhs:(883,4)-(889,42): Non-exhaustive patterns in function choose_univs

comment:4 in reply to:  3 ; Changed 9 years ago by chak

Replying to guest:

Also interested in this. Will the implementation allow varying non-instance types?

What do you mean by "varying non-instance type"? Whether you write

data family Blah x y :: *

or

data family Blah x :: * -> *

makes no difference whatsoever for data families.

comment:5 Changed 9 years ago by guest

Ah, ok.

By varying non-instance types, I meant are the constructors allowed to refine the types that don't index the family. However I've just realised/remembered there isn't a distinction between the named and kind-annotated types - my mistake.

I guess I was thinking that named variables somehow index the data family, (as with type families) and so you could determine which instance to use, and whether one is uniquely determined by a signature.

Just to totally clarify - of the 3 programs below, the first is a type error and the other two are type ok and equivalent?

{-# LANGUAGE GADTs, TypeFamilies, KindSignatures #-}

data family Blah x a :: *

data instance Blah Char Int where
  Char1 :: Blah Char Int

data instance Blah Char Bool where
  Char2 :: Blah Char Bool

foo :: Blah Char a -> a
foo Char1 = 2
foo Char2 = False

vs

{-# LANGUAGE GADTs, TypeFamilies, KindSignatures #-}

data family Blah x :: * -> *

data instance Blah Char a where 
  Char1 :: Blah Char Int
  Char2 :: Blah Char Bool
  
foo :: Blah Char a -> a
foo Char1 = 2
foo Char2 = False

vs

{-# LANGUAGE GADTs, TypeFamilies, KindSignatures #-}

data family Blah x a :: * 

data instance Blah Char a where 
  Char1 :: Blah Char Int
  Char2 :: Blah Char Bool
  
foo :: Blah Char a -> a
foo Char1 = 2
foo Char2 = False

comment:6 Changed 9 years ago by simonpj

Correct, I think. You definitely can't mix data contructors from two different 'data instances'.

Simon

comment:7 Changed 9 years ago by chak

Yes, as Simon says, you are perfectly right about the three examples.

Just as a final remark on that topic, the reason why it is tempting to think that "naming" a parameter in a data family declaration makes a difference is because it does make a difference for a type family. This is a point where data families and type synonym families are fundamentally different. The underlying type theoretic rational derives from the fact that a data family always introduces a new type, whereas a synonym family doesn't. A secondary consequence is that data families may be applied partially, whereas a synonym family must always be applied to at least as many type arguments as its arity (i.e., the number of named parameters in the declaration).

comment:8 Changed 9 years ago by chak

Test Case: GADT13

comment:9 Changed 8 years ago by simonmar

Architecture: MultipleUnknown/Multiple

comment:10 Changed 8 years ago by simonmar

Operating System: MultipleUnknown/Multiple

comment:11 in reply to:  4 Changed 8 years ago by jeltsch

Cc: g9ks157k@… added

Replying to chak:

What do you mean by "varying non-instance type"? Whether you write data family Blah x y :: * or data family Blah x :: * -> * makes no difference whatsoever for data families.

I think it does make a difference if you use associated types. Consider this:

{-# LANGUAGE TypeFamilies, GADTs #-}

class C t where

    data D t :: * -> *

instance C Bool where

    data D Bool Int = A

This doesn’t work, since the compiler expects a type variable at the place of the Int. Even more, you cannot introduce another constructor which constructs a D Bool Char, for example. With GADT syntax allowed in data family instance declarations, you could write the following:

{-# LANGUAGE TypeFamilies, GADTs #-}

class C t where

    data D t :: * -> *

instance C Bool where

    data D Bool where

        A :: D Bool Int

        B :: D Bool Char

This code would also be different to declaring two different data family instances (D Bool Int and D Bool Char) in that it makes it impossible to introduce, say, a D Bool Double instance later. This might be exactly what a library designer wants

I’d like to be able to use GADTs as data family instances for both of the above reasons. I think, I’d have good use for them.

comment:12 Changed 8 years ago by simonpj

Can we be more specific about what this ticket is about? The HEAD (but not 6.10) does indeed accept GADT syntax for data type families. (I implemented that a few months ago, but I think I forgot to tell anyone.) So the following program compiles fine; I believe it meets the hopes expressed by 'guest' and Wolfgang.

{-# LANGUAGE GADTs, TypeFamilies, KindSignatures #-}
module Foo where

data family Blah x :: * -> *

data instance Blah Char a where 
  Char1 :: Blah Char Int
  Char2 :: Blah Char Bool
  
foo :: Blah Char a -> a
foo Char1 = 2
foo Char2 = False

-------------------
class C t where
    data D t :: * -> *

instance C Bool where
    data D Bool a where
        A :: D Bool Int
        B :: D Bool Char

Does that do it? Shall we close the ticket? I've updated the docs to say explicitly that GADT syntax -- including actually defining a GADT as Wolfgang wants -- is allowed.

Simon

comment:13 in reply to:  12 Changed 8 years ago by jeltsch

Replying to simonpj:

Does that do it? Shall we close the ticket?

This seems to solve my problem. So as far as I’m concerned, this ticket can be closed. :-)

comment:14 in reply to:  12 Changed 8 years ago by TristanAllwood

Does everything I want, from my pov the ticket can be closed.

Cheers,

Tris ('guest')

comment:15 Changed 8 years ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: GADT13

OK, I'm closing this. Would one of you care to add a testsuite case (or submit a patch) so that we have a test for this feature?

I'm removing gadt13 as a test, since that test seems entirely unrelated to this ticket.

Simon

comment:16 Changed 8 years ago by jeltsch

Will this bug be fixed in GHC 6.10.2?

comment:17 Changed 8 years ago by igloo

The example in the original report works in the HEAD, but not the 6.10 branch.

comment:18 Changed 7 years ago by simonmar

difficulty: Moderate (1 day)Moderate (less than a day)
Note: See TracTickets for help on using tickets.