Odd ghc error message, “My brain just exploded”?

Question

When I try to pattern-match a GADT in an proc syntax (with Netwire and Vinyl):

sceneRoot = proc inputs -> do
            let (Identity camera :& Identity children) = inputs 
            returnA -< (<*>) (map (rGet draw) children) . pure

I get the (rather odd) compiler error, from ghc-7.6.3

  My brain just exploded
    I can't handle pattern bindings for existential or GADT data constructors.
    Instead, use a case-expression, or do-notation, to unpack the constructor.
    In the pattern: Identity cam :& Identity childs

I get a similar error when I put the pattern in the proc (...) pattern. Why is this? Is it unsound, or just unimplemented?

There seems to be some explanation in the source near where the error message is generated. — icktoofay
@DanielWagner: I would, but I'm not sure I understand it myself, and I'm not comfortable posting an answer I can't explain. — icktoofay

chi chi · Accepted Answer · 2014-05-08T11:25:55

Consider the GADT

data S a where
  S :: Show a => S a

and the execution of the code

foo :: S a -> a -> String
foo s x = case s of
            S -> show x

In a dictionary-based Haskell implementation, one would expect that the value s is carrying a class dictionary, and that the case extracts the show function from said dictionary so that show x can be performed.

If we execute

foo undefined (\x::Int -> 4::Int)

we get an exception. Operationally, this is expected, because we can not access the dictionary. More in general, case (undefined :: T) of K -> ... is going to produce an error because it forces the evaluation of undefined (provided that T is not a newtype).

Consider now the code (let's pretend that this compiles)

bar :: S a -> a -> String
bar s x = let S = s in show x

and the execution of

bar undefined (\x::Int -> 4::Int)

What should this do? One might argue that it should generate the same exception as with foo. If this were the case, referential transparency would imply that

let S = undefined :: S (Int->Int) in show (\x::Int -> 4::Int)

fails as well with the same exception. This would mean that the let is evaluating the undefined expression, very unlike e.g.

let [] = undefined :: [Int] in 5

which evaluates to 5.

Indeed, the patterns in a let are lazy: they do not force the evaluation of the expression, unlike case. This is why e.g.

let (x,y) = undefined :: (Int,Char) in 5

successfully evaluates to 5.

One might want to make let S = e in e' evaluate e if a show is needed in e', but it feels rather weird. Also, when evaluating let S = e1 ; S = e2 in show ... it would be unclear whether to evaluate e1, e2, or both.

GHC at the moment chooses to forbid all these cases with a simple rule: no lazy patterns when eliminating a GADT.

Odd ghc error message, “My brain just exploded”?

1 Answers