GADT problems

[Mitchell, Neil]

Hi Simon,

I appreciate that everything must be rigid, but am still confused. Given
the following operation:

op (Foo GadtValue) = ()

I can add a top-level type signature, and it works:

op :: Foo -> ()

But just putting those same type annotations in the actual function
doesn't work:

op (Foo GadtValue :: Foo) = () :: ()

From a simple point of view those two functions seem to have the same
amount of type information, but GHC gives different behaviour.

I think this is the underlying problem I'm getting. For things like
list-comps and cases I don't seem to be able to find any combination of
annotations that works, but that is because I'm not using top-level
annotations.

Thanks

Neil


> -----Original Message-----
> From: Simon Peyton-Jones [mailto:simonpj at microsoft.com] 
> Sent: 14 September 2008 3:11 pm
> To: Mitchell, Neil; glasgow-haskell-users at haskell.org
> Subject: RE: GADT problems
> 
> Neil
> 
> It's by design, and for (I think) good reason.   GHC now 
> enforces the rule that in a GADT pattern match
>         - the type of the scrutinee must be rigid
>         - the result type must be rigid
>         - the type of any variable free in the case branch 
> must be rigid
> 
> Here "rigid" means "fully known to the compiler, usually by 
> way of a type signature".  This rule is to make type 
> inference simple and predictable -- it dramatically 
> simplifies inference.
> 
> To see the issue, ask yourself what is the type of this function
> 
> data E a where
>   EI :: E Int
> 
> f EI = 3::Int
> 
> Should the inferred type be
>         f :: E a -> a
> or
>         f :: E a -> Int
> We can't tell, and neither is more general than the other.  
> So GHC insists on knowing the result type.  That's why you 
> had to give the signature g::[()] in your example.
> 
> 
> So that's the story.  If you find situations in which it's 
> very hard to give a signature for the result type, I'd like 
> to see them.
> 
> Dimitrios has just written an Appendix to our ICFP paper 
> about GADT inference, explaining the inference scheme -- it 
> is not otherwise written up anywhere.  I'll put it up shortly.
> 
> Thanks
> 
> Simon
> 
> | -----Original Message-----
> | From: glasgow-haskell-users-bounces at haskell.org 
> | [mailto:glasgow-haskell- users-bounces at haskell.org] On Behalf Of 
> | Mitchell, Neil
> | Sent: 12 September 2008 13:51
> | To: glasgow-haskell-users at haskell.org
> | Subject: GADT problems
> |
> | Hi
> |
> | The following code works in GHC 6.8.3, works in GHC 
> 6.9.20071111, but 
> | doesn't work in GHC HEAD.
> |
> | {-# LANGUAGE GADTs, ScopedTypeVariables #-}
> |
> | module Test where
> |
> | data E x = E x
> |
> | data Foo where
> |   Foo :: Gadt a -> Foo
> |
> | data Gadt a where
> |   GadtValue :: Gadt (E a)
> |
> | f (Foo GadtValue) = True
> | f _ = False
> |
> | Under GHC HEAD I get the error:
> |
> | GADT pattern match with non-rigid result type `t'
> |   Solution: add a type signature
> | In the definition of `f': f (Foo GadtValue) = True
> |
> | Adding a type signature to f fixes this problem:
> |
> | f :: Foo -> Bool
> |
> | But I haven't found anywhere other than the top level f to 
> add a type 
> | signature. When the match is in a list comprehension, it 
> becomes much 
> | harder. While playing further I discovered this example:
> |
> | foos = undefined
> | g = [() | Foo GadtValue <- foos]
> |
> | This code doesn't compile under GHC HEAD, but does under 6.8.3. 
> | However, adding the type signature:
> |
> | g :: [()]
> |
> | Makes the code compile. This is surprising, as [()] isn't a 
> GADT type, 
> | so shouldn't need stating explicitly.
> |
> | Any help on what these errors mean, or how they can be fixed with 
> | local type annotations?
> |
> | Thanks
> |
> | Neil
> |
> | 
> ======================================================================
> | =======
> | =
> | Please access the attached hyperlink for an important electronic 
> | communications disclaimer:
> |
> | http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html
> | 
> ======================================================================
> | =======
> | =
> |
> | _______________________________________________
> | Glasgow-haskell-users mailing list
> | Glasgow-haskell-users at haskell.org
> | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
> 
> 
> 

==============================================================================
Please access the attached hyperlink for an important electronic communications disclaimer: 

http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html
==============================================================================