id summary reporter owner description type status priority milestone component version resolution keywords cc os architecture failure testcase blockedby blocking related differential wikipage
8541 Coercible should be higher-kinded nomeata nomeata "Just discussed with SJP: The Coercible should be higher kinded, and it seems to be straight forward.
Given
{{{
data T f = T (f Int)
newtype List a = [a]
}}}
we want to be able to derive
{{{
Coercible (T (Either Int)) (T (Either Age))
Coercible (T List) (T [])
}}}
We now allow `Coercible` at a kind `* -> k`, with the following intuition:
{{{
Coercible A B ⇐⇒ (forall a. Coercible (A a) (B a))
}}}
Note that this is ok independent of the role of `A`’s parameter, as we are not modifying that parameter here.
Allowing such constraints, we therefore, we need these constraints exist in theory (but are in fact generated on demand, so only those of the rind kindnessare visible to the constraint solver) for `Either` and `List`:
{{{
instance (Coercible a b, Coercible c d)
=> Coercible (Either a c) (Either b d) -- old
instance Coercible a b => Coercible (Either a) (Either b) -- new
instance Coercible [a] b => Coercible (List a) b -- old
instance Coercible b [a] => Coercible b (List a) -- old
instance Coercible a b => Coercible (List a) (List b) -- old
instance Coercible [] b => Coercible List b -- new
instance Coercible b [] => Coercible b List -- new
}}}
This solves the cases above. It does not solve all cases, though. Consider
{{{
newtype NT1 a = NT1 (a -> Int)
newtype NT2 a = NT2 (a -> Int)
}}}
and we want to solve `Coercible (T NT1) (T NT2)`. Although, by the definition above, `Coercible NT1 NT2` should hold, such a coercion cannot be created (as far as I can see)." task closed normal Compiler 7.6.3 fixed goldfire Unknown/Multiple Unknown/Multiple None/Unknown TcCoercible, TcCoercibleFail3