Odd ghc error message, "My brain just exploded"?
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?
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 eg
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 eg
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 ... 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.
链接地址: http://www.djcxy.com/p/43074.html上一篇: GHC何时可以推断约束变量？