GADT problems

[Mitchell, Neil]

Hi

> | Ah, this is the crucial bit I've been misunderstanding! 
> Instinctively 
> | it feels that when a GADT can't type check I should be 
> annotating the 
> | GADT part - but that's not the case, I should be annotating the 
> | expression containing both the GADT match and its 
> right-hand side. I 
> | think the way the error message is formatted (add a type signature, 
> | followed by giving the local pattern) seems to hint at 
> this. With this 
> | insight I've managed to fix up all the real problems I was 
> experiencing.
> 
> Great.  Now you can help me!  Look at the documentation here 
> http://www.haskell.org/ghc/dist/current/docs/users_guide/data-
> type-extensions.html#gadt
> The last bullet.
> 
> What could I add that would eliminate your misunderstanding?  
>   You are in the ideal position to suggest concrete wording, 
> because you know the problem and the solution.  Examples are fine.

My mistunderstanding stems from:

(case undefined of Foo GadtValue -> ()) :: () -- is rigid

(case undefined of Foo GadtValue -> () :: ()) -- not rigid

The wording in the user manual is perfectly correct, but my intuition of
how rigidity propogates was wrong.

I'm also still not sure how the scrutinee (undefined in this case) is
rigid, when in your response you said undefined was very non-rigid.

An example in the user manual would be good, but having the compiler
identify where the missing type signature is would be significantly
better (albeit significantly more work). The example that would have
helped me is:

Given the case expression:

case scrutinee of
    GadtConstructor variable -> result

The potential type signatures that may be required to ensure rigidity
are:

(case scrutinee :: t of
     GadtConstructor (variable :: t) -> result) :: t


> You need a type signature for the scrutinee.  For example, this works:
> 
>   g :: [()]
>   g = [() | Foo (GadtValue _) <- undefined :: [Foo (E ())]]
> 
> Does that help?  Again, what words would help in the user manual.

In this particular case I don't fully understand the implications,
because the example is fake. If I encounter these issues in real code,
I'll take another look.

Thanks

Neil

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

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