GADTs and type synonyms

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|

GADTs and type synonyms

Ralf Hinze
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
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Reply | Threaded
Open this post in threaded view
|

RE: 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: [hidden email]
[mailto:glasgow-haskell-bugs-
| [hidden email]] On Behalf Of Ralf Hinze
| Sent: 28 December 2005 07:11
| To: [hidden email]
| 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
| [hidden email]
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs