<div dir="ltr"><div dir="ltr">Hello,<div><br></div><div>I assume the arguments to `reify` are meant to be the other way around?</div><div><br></div><div>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?</div><div><br></div><div><div>{-# Language ScopedTypeVariables #-}</div><div>{-# Language RankNTypes #-}</div><div>{-# Language TypeApplications #-}</div><div>{-# Language MultiParamTypeClasses #-}</div><div>{-# Language FlexibleContexts #-}</div><div>{-# Language AllowAmbiguousTypes #-}</div><div><br></div><div>class Reifies s a</div><div><br></div><div>reify :: forall a r. a -> (forall s. Reifies s a => r) -> r</div><div>reify _ _ = undefined</div><div><br></div><div>reflect :: forall s a. Reifies s a => a</div><div>reflect = undefined</div><div><br></div><div>example = reify 5 val</div><div>  where</div><div>  val :: forall s. Reifies s Integer => Integer</div><div>  val = reflect @s + reflect @s</div><div><br></div><div><br></div></div><div><br></div><div><br></div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Feb 22, 2019 at 9:55 AM Vladislav Zavialov <<a href="mailto:vlad.z.4096@gmail.com">vlad.z.4096@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">> isn't it the case that you could write it with scoped type variables if you wrote the type down?<br>
<br>
I don't think so, the type does not necessarily mention the type<br>
variables. For example, imagine we removed Proxy from reflection:<br>
<br>
  reify :: forall a r. a -> (forall s. Reifies s a => r) -> r<br>
  reflect :: forall s a. Reifies s a => a<br>
<br>
Under this proposal, I would be able to write<br>
<br>
  x = reify (\ @s -> reflect @s + reflect @s) (5 :: Integer)<br>
<br>
Here, x = 10 :: Integer.<br>
<br>
ScopedTypeVariables require extra Proxy arguments to express this,<br>
which are not only an inconvenience, but also extra data passed at<br>
runtime. Same reasoning applies to other higher-rank situations,<br>
including my other example with CPS-d proofs.<br>
<br>
All the best,<br>
- Vladislav<br>
</blockquote></div>