5

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.)

Theelepel
  • 193
  • 6
  • You don't need to explicitly introduce any type variable at all: `fooType (Foo x) = typeRep [x]` will also work, using the fact that the `proxy` for `typeRep` can be any functor: not necessarily the trivial `Proxy`, it can also be something that actually contains an `a` value! – leftaroundabout Sep 06 '17 at 15:14
  • 1
    @leftaroundabout if we're getting rid of the type variable, you can go even further and just say `fooType (Foo x) = typeOf x`. I went ahead and assumed the real use case was something where having access to the type variable was the important part. – Carl Sep 06 '17 at 15:17
  • 1
    @Carl yeah, but it's perhaps not that commonly known that _any_ function with `proxy x` argument can also be called with a concrete container containing an actual `x` value. – leftaroundabout Sep 06 '17 at 15:20
  • Indeed, I realize I can use `typeOf` or other solutions in this case (see last paragraph of the question in parentheses), but in my real code that is not available. I need to get a Template Haskell `Type` by putting the type variable in a type quote. I also can't bind `a` directly in the top function, because the type I am trying to get is actually a functional dependency of the hidden type. The helper function solution works fine, I just don't really understand why. – Theelepel Sep 06 '17 at 15:49
  • `let` can not do that, since it uses lazy pattern matching, and that can not bring typeclass dictionaries in scope. This is the same issue of https://stackoverflow.com/a/23540431/3234959 – chi Sep 06 '17 at 20:01

1 Answers1

10

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)
Carl
  • 26,500
  • 4
  • 65
  • 86
  • I can't use the provided solution in my code, but that explanation of case and let expressions does answer the question. It is a more elegant solution than using the helper function. Thanks! – Theelepel Sep 06 '17 at 16:00
  • Is STV even needed? `fooType (Foo x) = typeOf x` or `fooType (Foo x) = typeRep [x]` if you really want to use `typeRep` for some reason. – Daniel Wagner Sep 07 '17 at 00:06