Note [Ct kind invariant]

CEqCan requires that the kind of the lhs matches the kind
of the rhs. This is necessary because these constraints are used for substitutions
during solving. If the kinds differed, then the substitution would take a well-kinded
type to an ill-kinded one.