question about GADT's and error messages

[Andres Löh]

Hi.

Daniel is certainly right to point out general problems with GADT
pattern matching and principal types. Nevertheless, the changing
behaviour of GHC over time is currently a bit confusing to me.

In GHC-6.12.3, Doaitse's program fails with three errors (demo1,
demo2, demo4, all the GADT pattern matches without type signature),
and the error messages are:

/home/andres/trans/GT.hs:7:15:
    GADT pattern match in non-rigid context for `AInt'
      Probable solution: add a type signature for the scrutinee of the
case expression
    In the pattern: AInt i
    In a case alternative: (AInt i) -> print i
    In the expression: case a of { (AInt i) -> print i }

/home/andres/trans/GT.hs:33:18:
    GADT pattern match with non-rigid result type `t'
      Solution: add a type signature for the entire case expression
    In a case alternative: (AInt i) -> print i
    In the expression: case a of { (AInt i) -> print i }
    In the expression: do { case a of { (AInt i) -> print i } }

/home/andres/trans/GT.hs:41:18:
    GADT pattern match with non-rigid result type `t'
      Solution: add a type signature for the entire case expression
    In a case alternative: (AInt i) -> print i
    In the expression: case AInt 3 of { (AInt i) -> print i }
    In the expression: do { case AInt 3 of { (AInt i) -> print i } }

These error messages are conservative, but clear. They ask the user to
add a type signature.

With GHC-7.0.4, GHC-7.2.1, GHC-7.4.2, and GHC-7.6.3, the program
compiles without error, including demo1.

With GHC-7.8.2, the compiler reports the error Doaitse mentioned:

/home/andres/trans/GT.hs:7:27:
    Couldn't match expected type ‘t’ with actual type ‘IO ()’
      ‘t’ is untouchable
        inside the constraints (t1 ~ Int)

I think the error message would be more helpful if it would mention
adding a type signature as a possible fix again.

But, assuming for the time being that GHC is "correct" to reject this
program and that GHC-7 was "wrong" up until now, then I'd like to know
what the new rule for GADT pattern matching is. Obviously, it's more
relaxed than it used to be (because demo2 and demo4 are still
accepted). Also, am I correct that the OutsideIn JFP paper is still
the correct description of what's going on in the type checker? If so,
is GHC-7.6 or GHC-7.8 closer to implementing what the OutsideIn paper
describes? Is the change in behaviour documented somewhere?

Thanks.

Cheers,
  Andres

-- 
Andres Löh, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com

Registered in England & Wales, OC335890
250 Ice Wharf, 17 New Wharf Road, London N1 9RF, England