• simonpj's avatar
    [project @ 2003-12-30 16:29:17 by simonpj] · f714e6b6
    simonpj authored
            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
    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.