Why do Haskell's scoped type variables not allow binding of type variables in pattern bindings?

Question

I noticed that GHC's ScopedTypeVariables is able to bind type variables in function patterns but not let patterns.

As a minimal example, consider the type

data Foo where Foo :: Typeable a  => a -> Foo

If I want to gain access to the type inside a Foo, the following function does not compile:

fooType :: Foo -> TypeRep
fooType (Foo x) =
    let (_ :: a) = x
    in typeRep (Proxy::Proxy a)

But using this trick to move the type variable binding to a function call, it works without issue:

fooType (Foo x) =
    let helper (_ :: a) = typeRep (Proxy::Proxy a)
    in helper x

Since let bindings are actually function bindings in disguise, why aren't the above two code snippets equivalent?

(In this example, other solutions would be to create the TypeRep with typeOf x, or bind the variable directly as x :: a in the top-level function. Neither of those options are available in my real code, and using them doesn't answer the question.)

Answer 1

The big thing is, functions are case expressions in disguise, not let expressions. case matching and let matching have different semantics. This is also why you can't match a GADT constructor that does type refinement in a let expression.

The difference is that case matches evaluate the scrutinee before continuing, whereas let matches throw a thunk onto the heap that says "do this evaluation when the result is demanded". GHC doesn't know how to preserve locally-scoped types (like a in your example) across all the potential ways laziness may interact with them, so it just doesn't try. If locally-scoped types are involved, use a case expression such that laziness can't become a problem.

As for your code, ScopedTypeVariables actually provides you a far more succinct option:

{-# Language ScopedTypeVariables, GADTs #-}

import Data.Typeable
import Data.Proxy

data Foo where
    Foo :: Typeable a => a -> Foo

fooType :: Foo -> TypeRep
fooType (Foo (x :: a)) = typeRep (Proxy :: Proxy a)