My understanding of OutsideIn leads me to believe that GHC 7.8 has the behavior closer to that spec. See Section 5.2 of that paper (http://research.microsoft.com/en-us/um/people/simonpj/Papers/constraints/jfp...), which is a relatively accessible explanation of this phenomenon. Daniel's explanation is essentially a condensed version of that section.
I'm not surprised that the behavior changed between GHC 6.x and 7.x, as I believe 7.x is what brought in OutsideIn. I don't know much about the change between 7.6 and 7.8, though. And, I agree that the "untouchable" error messages are generally inscrutable. When I see that message in my own code, my takeaway is generally "I have a mistake somewhere near that line", nothing more specific or useful. I've accordingly posted a bug report #9109 (https://ghc.haskell.org/trac/ghc/ticket/9109). Please comment there if you have either useful examples or other contributions to the fix -- it may be hard to get this one right.
Richard
On May 13, 2014, at 5:51 PM, 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 _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users