GADT Strangeness

[Simon Peyton-Jones]

| If I remove -XScopedTypeVariables from this http://hpaste.org/13230 then
| I get the following error message:
|
| > Asn1cTestNew.hs:55:27:
| >     GADT pattern match in non-rigid context for `INTEGER'
| >       Solution: add a type signature
| >     In the pattern: INTEGER
| >     In the definition of `referenceTypeAndValAux2':
| >         referenceTypeAndValAux2 ns INTEGER x
| >                                   = lhs ns <> text " = " <> text (show x) <> semi
| > Failed, modules loaded: Language.ASN1, ASNTYPE.
|
| At the very least the message is unhelpful. It was only by accident I
| decided to put in -XScopedTypeVariables.

This one had me puzzled for a while too! Here is what's happening.

You have three mutually recursive functions:
        referenceTypeAndValAux1
        referenceTypeAndValAux2
        cSEQUENCE
In Haskell 98, typechecking mutually recursive functions is done *together*, with each having a momomorphic type in the other RHSs.  That leads to an annoying problem, that of figuring out how their polymorphic type variables "match up".  As a result, even the type variables in the type signature look non-rigid.

The solution is to use -XRelaxedPolyRec, which compiles mutually-recursive definitions that each have a type signature one by one.  Precisely because of the above infelicity, both -XGADTs and -XScopedTypeVariables imply -XRelaxedPolyRec.

This is a nasty corner I agree.  GHC requires -XGADTs for you to *define* a GADT. Perhaps it should also require -XGADTs for you to *match against* one (as you are doing here).  That would avoid this particular hole.  If you think that would be a step forward, do put forward a Trac feature request, and encourage others to support it.

Simon