GADTs and type synonyms

[Simon Peyton-Jones]

Hmm.  There's a question here.  Constructor args allow you to put
strictness annotations

  data Foo where
    MkFoo :: !Int -> !Bool -> Foo

You want to hide part of the declaration inside a type signature.   But
then what about the strictness annotations?   I suppose you could argue
for

  type Baz = !Bool -> Foo
  data Foo where
     MkFoo :: !Int -> Baz

But that's a new kind of 'type' declaration.  Maybe you could argue that
you should be allowed to use a type synonym when you don't need
strictness annotations, but that seems a bit of a hack.

So GHC currently insists that you write all the argument types of the
constructor, and the result, explicitly, with no type synonyms in the
way.  Do you think that's bad?  

The error message could be better I suppose.

Simon  

| -----Original Message-----
| From: glasgow-haskell-bugs-bounces at haskell.org
[mailto:glasgow-haskell-bugs-
| bounces at haskell.org] On Behalf Of Ralf Hinze
| Sent: 28 December 2005 07:11
| To: glasgow-haskell-bugs at haskell.org
| Subject: GADTs and type synonyms
| 
| Another GADT `bug report': type synonyms are not unfolded
| when checking the signature of the data constructors: given
| 
| > type Hello a = a -> a
| > data World :: * where
| >   Msg :: Hello World
| 
| GHC reports
| 
| GADT.lhs:2:1:
|     Data constructor `Msg' returns type `Hello'
|       instead of its parent type
|     When checking the data constructor: Msg
|     In the data type declaration for `World'
| 
| Applies to both version 6.4.1 and 6.5.
| 
| Cheers, Ralf
| _______________________________________________
| Glasgow-haskell-bugs mailing list
| Glasgow-haskell-bugs at haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs