Hello,

I assume the arguments to `reify` are meant to be the other way around?

Here is the ScopedTypeVariables version I thought should work but indeed it doesn't, although I don't fully understand why. Is it because GHC instantiates `val` and then tries to generalize again, but fails since the polymorphic argument to `reify` is very ambiguous? And is this the intended behavior?

{-# Language ScopedTypeVariables #-}

{-# Language RankNTypes #-}

{-# Language TypeApplications #-}

{-# Language MultiParamTypeClasses #-}

{-# Language FlexibleContexts #-}

{-# Language AllowAmbiguousTypes #-}

class Reifies s a

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

reify _ _ = undefined

reflect :: forall s a. Reifies s a => a

reflect = undefined

example = reify 5 val

where

val :: forall s. Reifies s Integer => Integer

val = reflect @s + reflect @s

On Fri, Feb 22, 2019 at 9:55 AM Vladislav Zavialov <vlad.z.4096@gmail.com> wrote:

> 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