How well do we skirt incoherence?

[treeowl]

It's possible to define instances of Reifies directly, and in fact Data.Reflection does so for some types. This kind of scares me. The existing instances get in the way by overlapping, but if you remove them for a moment, you can consider something horrifying like this:

instance Reifies (s :: *) Int where
  reflect _ = 12

Now if we have something like

f :: forall s proxy . Reifies s Int => proxy s -> Int
f p = reflect p

Well, GHC has an instance for that, so it can compile f directly to

f = /\ s proxy -> \ ( _ :: Reifies s Int) (_ :: proxy s) -> 12

If f is passed to reify, I don't think we get any guarantees.

Now as I mentioned, the current instances do get in the way of this horror by overlapping, which I believe prevents the premature specialization of f (s can't be shown to be apart from the various extant instances) but this whole thing makes me nervous, and I can't quite escape the nagging feeling that there could be some way to exploit it.

[mitchellwrosen]

@treeowl But GHC doesn't have an instance for that, because it doesn't exist in reflection. No hand-written instances can possibly "hook" into reify/reflect in a way that makes reflect give back something other than what was reify-ed. Parametricity!

[mitchellwrosen]

(Assuming you use the proxy s handed to you by reify. If you use some other proxy, of course you can get it to resolve to some other instance in scope. But why would you do that? :))

[treeowl]

@mitchellwrosen, my point is that, if not for the existing instances in reflection, a user could write such an instance. As it is, they cannot, which seems to save us. That just seems like a little bit of extra weirdness on top of everything else.

[mitchellwrosen]

@treeowl Even if no convenience instances existed in reflection, still no user could write such a "hook", by the same logic. I think I'm being unclear, sorry - on the train.

In your above example, the user-written Reifies instance is effectively dead code. The fundep is from s -> a, not a -> s.

[mitchellwrosen]

Oh! An overlapping instance on 's'. I see, I had my type variables backwards.