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?

Tagged in the example could be replaced with explicit type application if backwards compatibility isn't a concern. OTOH, it is.

Would that help Core typing?

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?

and admit both fundep and TF forms. I mean, if you're going to lie you might as well lie big.

Definitely.

There are a very large number of instances out there scattered across dozens of packages that would be broken by switching from Proxy to Tagged or explicit type application internally. (I realize that this is a lesser concern that can be resolved by a major version bump and some community friction, but it does mean pragmatically that migrating to something like this would need a plan.)

I just want to make sure that we do what we need to get Really Good Code, if we're going to the trouble of adding compiler support.