[project @ 2003-12-30 16:29:17 by simonpj]

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