[Haskell-cafe] Counterintuitive ScopedTypeVariables behaviour

[Alexis King]

I think this behavior is obscured by the way Haskell uses the term “type variable” to refer to three different things:

Variables that refer to types and are bound within the type namespace.

Skolem type constants introduced by a `forall`.

Solver/unification variables, aka “metavariables”, which aren’t really types at all but holes to be filled in with types.

These are all subtly different, but they are so frequently treated as if they were the same that I suspect listing them out is not actually enough for many people to understand the distinctions! So let me elaborate.

Suppose we view `forall` like a type-level lambda, so `forall a. a -> a` is analogous to this term:

\a -> a :-> a

Clearly, there is a difference between the variable `a` in the above expression and the value we eventually substitute for it when we apply the lambda. When we instantiate the function by doing, say, `id @Int`, we substitute `Int` for `a` to get `Int -> Int`. So `a` itself isn’t a type, it’s a name that refers to a type—a type variable.

Under this interpretation, there’s nothing wrong with your example. In

add (x :: a) (y :: b) = x + y

the variable `a` names `x`’s type, and the variable `b` names `y`’s type, and there’s nothing at all wrong with having two different names that refer to the same thing. It would be like writing this term:

\t -> let { a = t; b = t } in a :-> b

So why does it seem confusing? Well, because if we write

add :: Num t => a -> b -> t

we get a type error, not two aliases for t. This is because GHC will implicitly quantify all the variables in the type signature to get

add :: forall t a b. Num t => a -> b -> t

so `a` and `b` are now distinct, “lambda-bound” variables, not aliases for `t`.

This implicit quantification means we don’t often think about the type variables we write in type signatures as being like term variables, which are just names that reference other things. Rather, we think of type variables as being like type constants, and in fact GHC encourages this interpretation in its error reporting.

To explain, consider what happens when GHC checks `add` against the type we wrote above. Somehow, it needs to figure out the types of `x` and `y`, but it can’t just say

x :: a
y :: b

because those variables were bound by the `forall` (they are “lambda-bound”), and if we move them into some other context where they appear free, they no longer have any meaning. GHC has to somehow pick actual types for x and y, not type variables. A naïve idea would be to invent two new solver variables, aka “holes to be filled in with inferred types”, yielding something like

a1, b1 fresh
x :: a1
y :: b1

but this doesn’t work. Imagine we did that while typechecking this function:

bad :: a -> a
bad _ = True

If we invented a new solver variable to use in place of `a` while typechecking `bad`, GHC would just say “oh, I can fill in the hole with Bool” and carry on, which would be quite bad! The whole point of parametricity is that the function must work with any type.

So GHC actually does something else. Behind the scenes, it creates two new type definitions, distinct from all other types in the program:

data FakeTypeA
data FakeTypeB

Now it typechecks the function using these fake types substituted for `a` and `b`:

x :: FakeTypeA
y :: FakeTypeB

Now when GHC goes to typecheck `x + y`, it will raise a type error, since FakeTypeA and FakeTypeB are obviously not the same type. This enforces parametricity.

Of course, it would be very confusing to the user to see names like “FakeTypeA” in their type errors. So GHC pulls some sleight of hand, and it prints the new types it generates as just “a” and “b”, the same as the forall-bound variables it created them for. These don’t look like type constants, because in source Haskell, all type constants start with UpperCase. But behind the scenes, they really are type constants, not type variables. GHC calls these fake type constants “rigid variables” or “skolem variables,” but don’t be fooled: they’re not variables at all, they’re constants.

GHC tells this white lie to keep programmers from having to think about all this behind the scenes business. When GHC says “could not match ‘a’ with ‘b’,” it’s natural for programmers to think “ah, these are the ‘a’ and ‘b’ I wrote in my type signature,” and they learn to treat “type variables” and “rigid type constants” as one and the same. They don’t think about how this is a meaningfully different definition of “variable” than what they’re used to at the term level. This works out okay because the only way to bind type variables in source Haskell 98/2010 is universal quantification.

But now ScopedTypeVariables and ExistentialQuantification enter the picture, and there’s a problem: we suddenly need to be able to bind type variables in a place that isn’t `forall`. Now we have type variable binding sites that look just like type variable uses, but they aren’t implicitly-quantified the way they are in standalone type signatures, and confusion ensues.

This confusion actually goes much deeper than you might expect. Because Haskell historically hasn’t syntactically distinguished type variable uses from binding sites, we have new ambiguous situations like this:

\(x :: Maybe a) -> ...

Is this a type annotation on x, which states that x should have type `Maybe a`, where `a` is a type variable already in scope? Or is it a pattern binding that matches against x’s type, which asserts that it has the shape `Maybe t` and binds a new variable `a` to the type `t`? And it gets even worse! Suppose we have this:

f (Foo @a x) = ...

Is `@a` a visible type application of `Foo` to the in-scope type `a`, instantiating the (universally-quantified) `Foo` constructor at a particular type? Or is it a binder for an existential variable “stored inside” `Foo`? Both are reasonable (and useful) interpretations.

A GHC proposal that presents a design that sorts all these ambiguities out would be most welcome. To my knowledge, no such proposal currently exists, but I could be wrong—I know this issue has been discussed on some proposals (such as visible type applications in patterns), so maybe someone has come up with something I’m not aware of.

Alexis

> On Aug 16, 2020, at 07:17, Tom Ellis <tom-lists-haskell-cafe-2017 at jaguarpaw.co.uk> wrote:
> 
> I have just noticed that with ScopedTypeVariables one can write the
> following bizarre definition
> 
>    -- Inferred signature:
>    -- add :: Num a => a -> a -> a
>    add (x :: a) (y :: b) = x + y
> 
> The reason for this behaviour is that
> 
>> in all patterns other than pattern bindings, a pattern type
>> signature may mention a type variable that is not in scope; in this
>> case, the signature brings that type variable into scope.
> 
> https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#pattern-type-signatures
> 
> and the justification is that
> 
>> Bringing type variables into scope is particularly important for
>> existential data constructors
> 
> But this leads to a rather puzzling user experience.  Was it really
> not possible to design this extension in a way that would allow
> bringing new type variables into scope locally but not allow them to
> unify with other type variables from outer scopes?
> 
> To be more concrete, what I would like to see is a design where `k` is
> allowed because the type `a` (bound within a pattern) does not need to
> unify with anything but `k2` is not allowed because `a` is forbidden
> to unify with `b`.  `k3` would also be forbidden (the type variables
> called `a` are actually distinct) as would `k4` (the type variable for
> the inferred signature would be fresh and distinct from `a`).
> 
> I believe this design might lead to much less puzzling behaviour.
> Would it be possible (within a new extension, of course) or have I
> overlooked something?
> 
> Tom
> 
> 
>    data T = forall a. MkT [a]
> 
>    k :: T -> T
>    k (MkT [t::a]) =
>        MkT t3
>      where
>       (t3::[a]) = [t,t,t]
> 
>    data T2 a = MkT2 [a]
> 
>    k2 :: T2 b -> T2 b
>    k2 (MkT2 [t::a]) =
>        MkT2 t3
>      where
>       (t3::[a]) = [t,t,t]
> 
>    k3 :: T2 a -> T2 a
>    k3 (MkT2 [t::a]) =
>        MkT2 t3
>      where
>       (t3::[a]) = [t,t,t]
> 
>    k4 (MkT2 [t::a]) =
>        MkT2 t3
>      where
>       (t3::[a]) = [t,t,t]

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20200817/bdd659ca/attachment.html>