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-outsidein.pdf), 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 <and...@well-typed.com> wrote: > 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 > _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
