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.

3 files changed, 70 insertions, 54 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]
diff --git a/compiler/specialise/SpecConstr.hs b/compiler/specialise/SpecConstr.hs
index 1760b0e596..ff4613448e 100644
--- a/compiler/specialise/SpecConstr.hs
+++ b/compiler/specialise/SpecConstr.hs
@@ -31,13 +31,13 @@ import Literal          ( litIsLifted )
 import HscTypes         ( ModGuts(..) )
 import WwLib            ( mkWorkerArgs )
 import DataCon
-import Coercion         hiding( substTy, substCo )
+import Coercion         hiding( substCo )
 import Rules
 import Type             hiding ( substTy )
 import TyCon            ( isRecursiveTyCon, tyConName )
 import Id
 import PprCore          ( pprParendExpr )
-import MkCore           ( mkImpossibleExpr, sortQuantVars )
+import MkCore           ( mkImpossibleExpr )
 import Var
 import VarEnv
 import VarSet
@@ -1643,7 +1643,7 @@ spec_one env fn arg_bndrs body (call_pat@(qvars, pats), rule_number)
 --        return ()
 
                 -- And build the results
-        ; let spec_id    = mkLocalId spec_name (mkPiTypes spec_lam_args body_ty)
+        ; let spec_id    = mkLocalIdOrCoVar spec_name (mkPiTypes spec_lam_args body_ty)
                              -- See Note [Transfer strictness]
                              `setIdStrictness` spec_str
                              `setIdArity` count isId spec_lam_args
@@ -1850,7 +1850,7 @@ callToPats env bndr_occs (Call _ args con_env)
                 -- See Note [Shadowing] at the top
 
               (ktvs, ids)   = partition isTyVar qvars
-              qvars'        = sortQuantVars ktvs ++ map sanitise ids
+              qvars'        = toposortTyVars ktvs ++ map sanitise ids
                 -- Order into kind variables, type variables, term variables
                 -- The kind of a type variable may mention a kind variable
                 -- and the type of a term variable may mention a type variable
@@ -2001,7 +2001,7 @@ argToPat _env _in_scope _val_env arg _arg_occ
 wildCardPat :: Type -> UniqSM (Bool, CoreArg)
 wildCardPat ty
   = do { uniq <- getUniqueM
-       ; let id = mkSysLocal (fsLit "sc") uniq ty
+       ; let id = mkSysLocalOrCoVar (fsLit "sc") uniq ty
        ; return (False, varToCoreExpr id) }
 
 argsToPats :: ScEnv -> InScopeSet -> ValueEnv
diff --git a/compiler/specialise/Specialise.hs b/compiler/specialise/Specialise.hs
index cb671be7a5..d45b72a718 100644
--- a/compiler/specialise/Specialise.hs
+++ b/compiler/specialise/Specialise.hs
@@ -10,8 +10,8 @@ module Specialise ( specProgram, specUnfolding ) where
 #include "HsVersions.h"
 
 import Id
-import TcType hiding( substTy, extendTvSubstList )
-import Type   hiding( substTy, extendTvSubstList )
+import TcType hiding( substTy, extendTCvSubstList )
+import Type   hiding( substTy, extendTCvSubstList )
 import Coercion( Coercion )
 import Module( Module, HasModule(..) )
 import CoreMonad
@@ -21,7 +21,7 @@ import VarSet
 import VarEnv
 import CoreSyn
 import Rules
-import CoreUtils        ( exprIsTrivial, applyTypeToArgs )
+import CoreUtils        ( exprIsTrivial, applyTypeToArgs, mkCast )
 import CoreFVs          ( exprFreeVars, exprsFreeVars, idFreeVars )
 import UniqSupply
 import Name
@@ -858,7 +858,7 @@ specExpr env (Var v)       = return (specVar env v, emptyUDs)
 specExpr _   (Lit lit)     = return (Lit lit,       emptyUDs)
 specExpr env (Cast e co)
   = do { (e', uds) <- specExpr env e
-       ; return ((Cast e' (substCo env co)), uds) }
+       ; return ((mkCast e' (substCo env co)), uds) }
 specExpr env (Tick tickish body)
   = do { (body', uds) <- specExpr env body
        ; return (Tick (specTickish env tickish) body', uds) }
@@ -959,7 +959,7 @@ specCase env scrut' case_bndr [(con, args, rhs)]
     sc_args' = filter is_flt_sc_arg args'
 
     clone_me bndr = do { uniq <- getUniqueM
-                       ; return (mkUserLocal occ uniq ty loc) }
+                       ; return (mkUserLocalOrCoVar occ uniq ty loc) }
        where
          name = idName bndr
          ty   = idType bndr
@@ -970,7 +970,7 @@ specCase env scrut' case_bndr [(con, args, rhs)]
     is_flt_sc_arg var =  isId var
                       && not (isDeadBinder var)
                       && isDictTy var_ty
-                      && not (tyVarsOfType var_ty `intersectsVarSet` arg_set)
+                      && not (tyCoVarsOfType var_ty `intersectsVarSet` arg_set)
        where
          var_ty = idType var
 
@@ -1182,15 +1182,15 @@ specCalls mb_mod env rules_for_me calls_for_me fn rhs
                      , ppr rhs_ids, ppr n_dicts
                      , ppr (idInlineActivation fn) ]
 
-    fn_type            = idType fn
-    fn_arity           = idArity fn
-    fn_unf             = realIdUnfolding fn     -- Ignore loop-breaker-ness here
-    (tyvars, theta, _) = tcSplitSigmaTy fn_type
-    n_tyvars           = length tyvars
-    n_dicts            = length theta
-    inl_prag           = idInlinePragma fn
-    inl_act            = inlinePragmaActivation inl_prag
-    is_local           = isLocalId fn
+    fn_type                 = idType fn
+    fn_arity                = idArity fn
+    fn_unf                  = realIdUnfolding fn  -- Ignore loop-breaker-ness here
+    (tyvars, theta, _)      = tcSplitSigmaTy fn_type
+    n_tyvars                = length tyvars
+    n_dicts                 = length theta
+    inl_prag                = idInlinePragma fn
+    inl_act                 = inlinePragmaActivation inl_prag
+    is_local                = isLocalId fn
 
         -- Figure out whether the function has an INLINE pragma
         -- See Note [Inline specialisations]
@@ -1244,7 +1244,7 @@ specCalls mb_mod env rules_for_me calls_for_me fn rhs
                 -- spec_tyvars = [a,c]
                 -- ty_args     = [t1,b,t3]
                 spec_tv_binds = [(tv,ty) | (tv, Just ty) <- rhs_tyvars `zip` call_ts]
-                env1          = extendTvSubstList env spec_tv_binds
+                env1          = extendTCvSubstList env spec_tv_binds
                 (rhs_env, poly_tyvars) = substBndrs env1
                                             [tv | (tv, Nothing) <- rhs_tyvars `zip` call_ts]
 
@@ -1775,7 +1775,7 @@ singleCall id tys dicts
                      Map.singleton (CallKey tys) (dicts, call_fvs) }
   where
     call_fvs = exprsFreeVars dicts `unionVarSet` tys_fvs
-    tys_fvs  = tyVarsOfTypes (catMaybes tys)
+    tys_fvs  = tyCoVarsOfTypes (catMaybes tys)
         -- The type args (tys) are guaranteed to be part of the dictionary
         -- types, because they are just the constrained types,
         -- and the dictionary is therefore sure to be bound
@@ -1812,14 +1812,20 @@ mkCallUDs' env f args
   where
     _trace_doc = vcat [ppr f, ppr args, ppr n_tyvars, ppr n_dicts
                       , ppr (map (interestingDict env) dicts)]
-    (tyvars, theta, _) = tcSplitSigmaTy (idType f)
-    constrained_tyvars = closeOverKinds (tyVarsOfTypes theta)
-    n_tyvars           = length tyvars
-    n_dicts            = length theta
+    (tyvars, theta, _)      = tcSplitSigmaTy (idType f)
+    constrained_tyvars      = tyCoVarsOfTypes theta
+    n_tyvars                = length tyvars
+    n_dicts                 = length theta
 
-    spec_tys = [mk_spec_ty tv ty | (tv, Type ty) <- tyvars `zip` args]
+    spec_tys = [mk_spec_ty tv ty | (tv, ty) <- tyvars `type_zip` args]
     dicts    = [dict_expr | (_, dict_expr) <- theta `zip` (drop n_tyvars args)]
 
+    -- ignores Coercion arguments
+    type_zip :: [TyVar] -> [CoreExpr] -> [(TyVar, Type)]
+    type_zip tvs      (Coercion _ : args) = type_zip tvs args
+    type_zip (tv:tvs) (Type ty : args)    = (tv, ty) : type_zip tvs args
+    type_zip _        _                   = []
+
     mk_spec_ty tyvar ty
         | tyvar `elemVarSet` constrained_tyvars = Just ty
         | otherwise                             = Nothing
@@ -2131,9 +2137,9 @@ mapAndCombineSM f (x:xs) = do (y, uds1) <- f x
                               (ys, uds2) <- mapAndCombineSM f xs
                               return (y:ys, uds1 `plusUDs` uds2)
 
-extendTvSubstList :: SpecEnv -> [(TyVar,Type)] -> SpecEnv
-extendTvSubstList env tv_binds
-  = env { se_subst = CoreSubst.extendTvSubstList (se_subst env) tv_binds }
+extendTCvSubstList :: SpecEnv -> [(TyVar,Type)] -> SpecEnv
+extendTCvSubstList env tv_binds
+  = env { se_subst = CoreSubst.extendTCvSubstList (se_subst env) tv_binds }
 
 substTy :: SpecEnv -> Type -> Type
 substTy env ty = CoreSubst.substTy (se_subst env) ty
@@ -2175,7 +2181,7 @@ newDictBndr :: SpecEnv -> CoreBndr -> SpecM CoreBndr
 newDictBndr env b = do { uniq <- getUniqueM
                        ; let n   = idName b
                              ty' = substTy env (idType b)
-                       ; return (mkUserLocal (nameOccName n) uniq ty' (getSrcSpan n)) }
+                       ; return (mkUserLocalOrCoVar (nameOccName n) uniq ty' (getSrcSpan n)) }
 
 newSpecIdSM :: Id -> Type -> SpecM Id
     -- Give the new Id a similar occurrence name to the old one
@@ -2183,7 +2189,7 @@ newSpecIdSM old_id new_ty
   = do  { uniq <- getUniqueM
         ; let name    = idName old_id
               new_occ = mkSpecOcc (nameOccName name)
-              new_id  = mkUserLocal new_occ uniq new_ty (getSrcSpan name)
+              new_id  = mkUserLocalOrCoVar new_occ uniq new_ty (getSrcSpan name)
         ; return new_id }
 
 {-