| - Is it sound to apply a coercion (such as :Co:TFunctor) to a type | whose kind is a subkind of its argument kind? I would have thought no, | but you seem to be implying yes.
Sure! If Car is a subtype of Vehicle, and f :: Vehicle -> Int, then applying f to a Car is fine. That's just the ordinary contravariance rule for subtyping | - Does anything actually go wrong if you do? Well, since it seems sound in general, I guess no. | But I'm not so sure that it's sound in general. What if you had a coercion like: | :CoT (t:::*) (forall a . a -> t :=: a -> T) | where T :: *? | Then if you wrote (:CoT (u::?)), That's ill-kinded, because ? is not sub-kind of *. In my earlier example, * is like Car, and ? is like Vehicle. You can't give a Vehicle to a function expecting a Car! Simon _______________________________________________ Cvs-ghc mailing list [email protected] http://www.haskell.org/mailman/listinfo/cvs-ghc
