question about GADT's and error messages

[Richard Eisenberg]

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 <andres at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>