Add kind equalities to GHC.

This implements the ideas originally put forward in
"System FC with Explicit Kind Equality" (ICFP'13).

There are several noteworthy changes with this patch:
 * We now have casts in types. These change the kind
   of a type. See new constructor `CastTy`.

 * All types and all constructors can be promoted.
   This includes GADT constructors. GADT pattern matches
   take place in type family equations. In Core,
   types can now be applied to coercions via the
   `CoercionTy` constructor.

 * Coercions can now be heterogeneous, relating types
   of different kinds. A coercion proving `t1 :: k1 ~ t2 :: k2`
   proves both that `t1` and `t2` are the same and also that
   `k1` and `k2` are the same.

 * The `Coercion` type has been significantly enhanced.
   The documentation in `docs/core-spec/core-spec.pdf` reflects
   the new reality.

 * The type of `*` is now `*`. No more `BOX`.

 * Users can write explicit kind variables in their code,
   anywhere they can write type variables. For backward compatibility,
   automatic inference of kind-variable binding is still permitted.

 * The new extension `TypeInType` turns on the new user-facing
   features.

 * Type families and synonyms are now promoted to kinds. This causes
   trouble with parsing `*`, leading to the somewhat awkward new
   `HsAppsTy` constructor for `HsType`. This is dispatched with in
   the renamer, where the kind `*` can be told apart from a
   type-level multiplication operator. Without `-XTypeInType` the
   old behavior persists. With `-XTypeInType`, you need to import
   `Data.Kind` to get `*`, also known as `Type`.

 * The kind-checking algorithms in TcHsType have been significantly
   rewritten to allow for enhanced kinds.

 * The new features are still quite experimental and may be in flux.

 * TODO: Several open tickets: #11195, #11196, #11197, #11198, #11203.

 * TODO: Update user manual.

Tickets addressed: #9017, #9173, #7961, #10524, #8566, #11142.
Updates Haddock submodule.

1 files changed, 32 insertions, 22 deletions

diff --git a/compiler/specialise/Rules.hs b/compiler/specialise/Rules.hs
index f7a67ea8bd..531b13166c 100644
--- a/compiler/specialise/Rules.hs
+++ b/compiler/specialise/Rules.hs
@@ -37,7 +37,7 @@ import CoreFVs          ( exprFreeVars, exprsFreeVars, bindFreeVars
 import CoreUtils        ( exprType, eqExpr, mkTick, mkTicks,
                           stripTicksTopT, stripTicksTopE )
 import PprCore          ( pprRules )
-import Type             ( Type, substTy, mkTvSubst )
+import Type             ( Type, substTy, mkTCvSubst )
 import TcType           ( tcSplitTyConApp_maybe )
 import TysPrim          ( anyTypeOfKind )
 import Coercion
@@ -50,7 +50,7 @@ import VarSet
 import Name             ( Name, NamedThing(..), nameIsLocalOrFrom )
 import NameSet
 import NameEnv
-import Unify            ( ruleMatchTyX, MatchEnv(..) )
+import Unify            ( ruleMatchTyX )
 import BasicTypes       ( Activation, CompilerPhase, isActive, pprRuleName )
 import StaticFlags      ( opt_PprStyle_Debug )
 import DynFlags         ( DynFlags )
@@ -61,6 +61,7 @@ import Bag
 import Util
 import Data.List
 import Data.Ord
+import Control.Monad    ( guard )
 
 {-
 Note [Overall plumbing for rules]
@@ -561,7 +562,17 @@ matchN (in_scope, id_unf) rule_name tmpl_vars tmpl_es target_es
              -- See Note [Unbound template type variables]
         where
           fake_ty = anyTypeOfKind kind
-          kind = Type.substTy (mkTvSubst in_scope tv_subst) (tyVarKind tmpl_var)
+          cv_subst = to_co_env id_subst
+          kind = Type.substTy (mkTCvSubst in_scope (tv_subst, cv_subst))
+                              (tyVarKind tmpl_var)
+
+          to_co_env env = foldVarEnv_Directly to_co emptyVarEnv env
+          to_co uniq expr env
+            | Just co <- exprToCoercion_maybe expr
+            = extendVarEnv_Directly env uniq co
+
+            | otherwise
+            = env
 
     unbound var = pprPanic "Template variable unbound in rewrite rule" $
                   vcat [ ptext (sLit "Variable:") <+> ppr var
@@ -779,19 +790,20 @@ match_co :: RuleMatchEnv
          -> Coercion
          -> Coercion
          -> Maybe RuleSubst
-match_co renv subst (CoVarCo cv) co
-  = match_var renv subst cv (Coercion co)
-match_co renv subst (Refl r1 ty1) co
-  = case co of
-       Refl r2 ty2
-         | r1 == r2 -> match_ty renv subst ty1 ty2
-       _            -> Nothing
-match_co renv subst (TyConAppCo r1 tc1 cos1) co2
-  = case co2 of
-       TyConAppCo r2 tc2 cos2
-         | r1 == r2 && tc1 == tc2
-         -> match_cos renv subst cos1 cos2
-       _ -> Nothing
+match_co renv subst co1 co2
+  | Just cv <- getCoVar_maybe co1
+  = match_var renv subst cv (Coercion co2)
+  | Just (ty1, r1) <- isReflCo_maybe co1
+  = do { (ty2, r2) <- isReflCo_maybe co2
+       ; guard (r1 == r2)
+       ; match_ty renv subst ty1 ty2 }
+match_co renv subst co1 co2
+  | Just (tc1, cos1) <- splitTyConAppCo_maybe co1
+  = case splitTyConAppCo_maybe co2 of
+      Just (tc2, cos2)
+        |  tc1 == tc2
+        -> match_cos renv subst cos1 cos2
+      _ -> Nothing
 match_co _ _ _co1 _co2
     -- Currently just deals with CoVarCo, TyConAppCo and Refl
 #ifdef DEBUG
@@ -806,13 +818,11 @@ match_cos :: RuleMatchEnv
          -> [Coercion]
          -> Maybe RuleSubst
 match_cos renv subst (co1:cos1) (co2:cos2) =
-    case match_co renv subst co1 co2 of
-       Just subst' -> match_cos renv subst' cos1 cos2
-       Nothing -> Nothing
+  do { subst' <- match_co renv subst co1 co2
+     ; match_cos renv subst' cos1 cos2 }
 match_cos _ subst [] [] = Just subst
 match_cos _ _ cos1 cos2 = pprTrace "match_cos: not same length" (ppr cos1 $$ ppr cos2) Nothing
 
-
 -------------
 rnMatchBndr2 :: RuleMatchEnv -> RuleSubst -> Var -> Var -> RuleMatchEnv
 rnMatchBndr2 renv subst x1 x2
@@ -932,11 +942,11 @@ match_ty :: RuleMatchEnv
 -- We only want to replace (f T) with f', not (f Int).
 
 match_ty renv subst ty1 ty2
-  = do  { tv_subst' <- Unify.ruleMatchTyX menv tv_subst ty1 ty2
+  = do  { tv_subst'
+            <- Unify.ruleMatchTyX (rv_tmpls renv) (rv_lcl renv) tv_subst ty1 ty2
         ; return (subst { rs_tv_subst = tv_subst' }) }
   where
     tv_subst = rs_tv_subst subst
-    menv = ME { me_tmpls = rv_tmpls renv, me_env = rv_lcl renv }
 
 {-
 Note [Expanding variables]