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

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