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

by

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.

More Related Contents:

  1. Why give me error? [closed]
  2. What is the difference between . (dot) and $ (dollar sign)?
  3. Good examples of Not a Functor/Functor/Applicative/Monad?
  4. Haskell ranges and floats
  5. Defining a function by equations with different number of arguments
  6. :sprint for polymorphic values?
  7. Small Haskell program compiled with GHC into huge binary
  8. Multi-line commands in GHCi
  9. Writing foldl using foldr
  10. What does the exclamation mark mean in a Haskell declaration?
  11. Haskell function composition operator of type (c→d) → (a→b→c) → (a→b→d)
  12. Haskell: Lists, Arrays, Vectors, Sequences
  13. What are “n+k patterns” and why are they banned from Haskell 2010?
  14. How do I write, “if typeclass a, then a is also an instance of b by this definition.”
  15. Haskell read raw keyboard input
  16. Currying 3 Arguments in Haskell
  17. Applicative functor evaluation is not clear to me
  18. Expressing do block using only monadic bind syntax
  19. Why do we need monads?
  20. What constitutes a fold for types other than list?
  21. Defining a new monad in haskell raises no instance for Applicative
  22. How to make a CAF not a CAF in Haskell?
  23. Check whether a type is an instance of Show in Haskell at runtime?
  24. Integral operators quot vs. div
  25. How to interpret bind/>>= of the function instance?
  26. Why should Applicative be a superclass of Monad?
  27. withFile vs. openFile
  28. Why does OCaml sometimes require eta expansion?
  29. Does Haskell have return type overloading?
  30. What is predicativity?

Leave a Comment