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 _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users