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