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

[Iavor Diatchki]

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 at 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20190222/af1bab8c/attachment.html>