[ghc-steering-committee] Discussion on #155 Type Variable in Labmdas

[Vladislav Zavialov]

> isn't it the case that you could write it with scoped type variables if you wrote the type down?

I don't think so, the type does not necessarily mention the type
variables. For example, imagine we removed Proxy from reflection:

  reify :: forall a r. a -> (forall s. Reifies s a => r) -> r
  reflect :: forall s a. Reifies s a => a

Under this proposal, I would be able to write

  x = reify (\ @s -> reflect @s + reflect @s) (5 :: Integer)

Here, x = 10 :: Integer.

ScopedTypeVariables require extra Proxy arguments to express this,
which are not only an inconvenience, but also extra data passed at
runtime. Same reasoning applies to other higher-rank situations,
including my other example with CPS-d proofs.

All the best,
- Vladislav