Coercible should be higher-kinded

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).

Trac metadata

Trac field	Value
Version	7.6.3
Type	Task
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	goldfire
Operating system
Architecture