[project @ 2003-12-30 16:29:17 by simonpj]
---------------------------- Re-do kind inference (again) ---------------------------- [WARNING: interface file binary representation has (as usual) changed slightly; recompile your libraries!] Inspired by the lambda-cube, for some time GHC has used type Kind = Type That is, kinds were represented by the same data type as types. But GHC also supports unboxed types and unboxed tuples, and these complicate the kind system by requiring a sub-kind relationship. Notably, an unboxed tuple is acceptable as the *result* of a function but not as an *argument*. So we have the following setup: ? / \ / \ ?? (#) / \ * # where * [LiftedTypeKind] means a lifted type # [UnliftedTypeKind] means an unlifted type (#) [UbxTupleKind] means unboxed tuple ?? [ArgTypeKind] is the lub of *,# ? [OpenTypeKind] means any type at all In particular: error :: forall a:?. String -> a (->) :: ?? -> ? -> * (\(x::t) -> ...) Here t::?? (i.e. not unboxed tuple) All this has beome rather difficult to accommodate with Kind=Type, so this commit splits the two. * Kind is a distinct type, defined in types/Kind.lhs * IfaceType.IfaceKind disappears: we just re-use Kind.Kind * TcUnify.unifyKind is a distinct unifier for kinds * TyCon no longer needs KindCon and SuperKindCon variants * TcUnify.zapExpectedType takes an expected Kind now, so that in TcPat.tcMonoPatBndr we can express that the bound variable must have an argTypeKind (??). The big change is really that kind inference is much more systematic and well behaved. In particular, a kind variable can unify only with a "simple kind", which is built from * and (->). This deals neatly with awkward questions about how we can combine sub-kinding with type inference. Lots of small consequential changes, especially to the kind-checking plumbing in TcTyClsDecls. (We played a bit fast and loose before, and now we have to be more honest, in particular about how kind inference works for type synonyms. They can have kinds like (* -> #), so This cures two long-standing SourceForge bugs * 753777 (tcfail115.hs), which used erroneously to pass, but crashed in the code generator type T a = Int -> (# Int, Int #) f :: T a -> T a f t = \x -> case t x of r -> r * 753780 (tc167.hs), which used erroneously to fail f :: (->) Int# Int# Still, the result is not entirely satisfactory. In particular * The error message from tcfail115 is pretty obscure * SourceForge bug 807249 (Instance match failure on openTypeKind) is not fixed. Alas.