Improve Coercible under foralls
Consider
newtype Age = MkAge Int
h :: forall m. m Int -> m Age
h x = coerce @(m Int) @(m Age) x
This fails, as it should, with
Couldn't match representation of type 'm Int'
with that of 'm Age'
arising from a use of 'coerce'
NB: We cannot know what roles the parameters to 'm' have;
we must assume that the role is nominal
And indeed, if we have
type family F a
data T a = MkT (F a)
Then h @T
would indeed be bogus because T Int
and T Age
might have very different representations.
So far so good. Now consider
f :: forall m. (forall p q. Coercible p q => Coercible (m p) (m q))
=> m Int -> m Age
f x = coerce @(m Int) @(m Age) x
g :: forall m. (forall p q. Coercible p q => Coercible (m p) (m q))
=> (forall a. a -> m Int) -> (forall a. a-> m Age)
g x = coerce @(forall a. a -> m Int) @(forall a. a -> m Age) x
Here f
succeeds. It needs [W] Coercible (m Int) (m Age)
which it can prove from the quantified constraint.
But g
is rejected with
Couldn't match representation of type 'm Int'
with that of 'm Age'
arising from a use of 'coerce'
NB: We cannot know what roles the parameters to 'm' have;
we must assume that the role is nominal
In the expression:
coerce @(forall a. a -> m Int) @(forall a. a -> m Age) x
That's odd! I can easily come up with a succesful elaboration of the program. Why? We start from
[W] Coercible (forall a. a -> m Int) (forall a. a -> m Age)
===>
[W] (forall a. a -> m Int) ~R# (forall a. a -> m Age)
===> {make an implication constraint}
[W] forall <noev> a. () => (a -> m Int) ~R# (a -> m Age)
The <noev>
says that we don't have a place to put value-level evidence. Then we decompose:
===>
[W] forall <noev> a. () => (m Int) ~R# (m Age)
and now we are stuck because there is nowhere to put the evidence.
But the solution is simple! Just float the constraint out of the implication (it does not mention the skolem a
). I have done this in !3319, and indeed it works.
However, it doesn't solve the full problem. What we wanted m a Int ~R# m a Age
? Now the skolem a
would prevent the constraint floating out, and we are back to square 1
That term-level quantified constraint (forall p q. Coercible p q => Coercible (m p) (m q))
is really a way of saying "m's first argument has representational role". Perhaps we should seek a way of saying that more directly, and in a way we can use in coercions. Something like Rep# m
. Then the evidence for Rep# m
justifies decomposing a wanted constraint m t1 ~R# m t2
.
Another alternative would be to decorate the arrow in m's kind, as we proposed in the first roles paper.
Neither seems simple. So this ticket is just recording the issue, and pointing to the MR, for posterity.
All this arose in #18148 and #18213, but is only tangentially related in the end.