data family + GADT: not implemented yet

[Remi]

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

[chak]

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.

[guest]

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

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

[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

[simonpj]

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

Simon

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

[jeltsch]

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.

[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

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

[TristanAllwood]

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

Cheers,

Tris ('guest')

[simonpj]

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

[jeltsch]

Will this bug be fixed in GHC 6.10.2?

[igloo]

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