21

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?

user1118321
  • 25,567
  • 4
  • 55
  • 86
Dan
  • 12,409
  • 3
  • 50
  • 87
  • 3
    There seems to be [some explanation in the source](https://github.com/ghc/ghc/blob/17c955402871862dea5021e0b83b0949da5e51e7/compiler/typecheck/TcPat.lhs#L1012) near [where the error message is generated](https://github.com/ghc/ghc/blob/17c955402871862dea5021e0b83b0949da5e51e7/compiler/typecheck/TcPat.lhs#L1118). – icktoofay May 08 '14 at 02:22
  • I think `->` should be `$`. – bisserlis May 08 '14 at 02:33
  • @bisserlis: No, it's [arrow syntax](http://www.haskell.org/arrows/syntax.html). – icktoofay May 08 '14 at 02:37
  • Oh fascinating! I've never seen this extension before. After a quick search, the [vinyl docs for Rec](http://hackage.haskell.org/package/vinyl-0.3/docs/src/Data-Vinyl-Rec.html#Rec) indicate that `:&` was defined as a GADT data constructor. If you switch to using a case statement the problem should evaporate. – bisserlis May 08 '14 at 03:14
  • @icktoofay Copy some text from there to here and make it an answer! – Daniel Wagner May 08 '14 at 03:50
  • 1
    @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 May 08 '14 at 04:15
  • 1
    Related answer: http://stackoverflow.com/a/213441/1651941 – Sibi May 08 '14 at 05:27

1 Answers1

12

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.

chi
  • 111,837
  • 3
  • 133
  • 218
  • 1
    The last example (with multiple `let`s) is closer to the reason given in the ghc source. The simple approach (from the typechecker's standpoint) is to combine all the constraints into a single context. But in some cases that simplification is not valid. So currently those cases are disallowed. – John L May 09 '14 at 00:41