On Thu, Dec 22, 2016 at 4:58 PM, Edward Kmett <ekmett@gmail.com> wrote:
> On Mon, Dec 12, 2016 at 1:31 PM, David Feuer <david.feuer@gmail.com> wrote:
>>
>> On Dec 12, 2016 1:15 PM, "Edward Kmett" <ekmett@gmail.com> wrote:
>>
>> A few thoughts in no particular order:
>>
>> Unlike this proposal, the existing 'reify' itself as core can actually be
>> made well typed.
>>
>>
>> Can you explain this?
>
> I mean just that. If you look at the core generated by the existing 'reify'
> combinator, nothing it does is 'evil'. We're allowing it to construct a
> dictionary. That isn't unsound where core is concerned.

So what *is* evil about my Tagged approach? Or do you just mean that
the excessive polymorphism is evil? There's no doubt that it is, but
the only ways I see to avoid it are to bake in a particular Reifies
class, which is a different kind of evil, or to come up with a way to
express the constraint that the class has exactly one method, which is
Extreme Overkill.

> Where the surface language is concerned the uniqueness of that dictionary is
> preserved by the quantifier introducing a new type generatively in the local
> context, so the usual problems with dictionary construction are defused.

>>  On the other other hand, if you're going to be magic, you might as well
>> go all the way to something like:
>>
>> reify# :: (p => r) -> a -> r
>>
>>
>> How would we implement reify in terms of this variant?
>
> That I don't have the answer to. It seems like it should work though.

I think it does. I've changed the reify# type a bit to avoid an
ambiguity I couldn't resolve.

newtype Constrain p r = Constrain (p => r)

reify# :: Constrain p r -> a -> r

Using my Tagged definition of Reifies, we get

reify' :: forall a r . (forall s . Reifies s a => Tagged s r) -> a -> r
reify' f = reify# (Constrain (unTagged (f :: Tagged s r)) :: forall s
. Constrain (Reifies s a) r)

reify :: forall a r . a -> (forall s . Reifies s a => Proxy s -> r) -> r
reify a f = reify# (Constrain (f (Proxy :: Proxy s)) :: forall s .
Constrain (Reifies s a) r) a

Using your proxy version, things are trickier, but I think it's

reify :: forall a r . a -> (forall s . Reifies s a => Proxy s -> r) -> r
reify a f = (reify# (Constrain (f (Proxy :: Proxy s)) :: forall s .
Constrain (Reifies s a) r)) (const a :: forall proxy s . proxy s -> a)

David