GADT problems

[Simon Peyton-Jones]

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

No, the former isn't rigid either.  BOTH the scrutinee AND the return type must be rigid, and in the former case the scrutinee does not have a rigid type.

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

Quite right.  See my comment above.

| 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

OK.  Can you give a sample program and the error message you'd like to see?

If you can suggest improvements to the manual I'm all ears.  Notably, it says nothing about what "rigid" means or how it propagates.

Simon