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, 186 insertions, 98 deletions

diff --git a/compiler/coreSyn/CoreFVs.hs b/compiler/coreSyn/CoreFVs.hs
index 398f6bee39..bf5d773a66 100644
--- a/compiler/coreSyn/CoreFVs.hs
+++ b/compiler/coreSyn/CoreFVs.hs
@@ -22,9 +22,10 @@ module CoreFVs (
         exprSomeFreeVars, exprsSomeFreeVars,
 
         -- * Free variables of Rules, Vars and Ids
-        varTypeTyVars,
-        varTypeTyVarsAcc,
-        idUnfoldingVars, idFreeVars, idRuleAndUnfoldingVars,
+        varTypeTyCoVars,
+        varTypeTyCoVarsAcc,
+        idUnfoldingVars, idFreeVars, dIdFreeVars,
+        idRuleAndUnfoldingVars, idRuleAndUnfoldingVarsDSet,
         idFreeVarsAcc,
         idRuleVars, idRuleRhsVars, stableUnfoldingVars,
         ruleRhsFreeVars, ruleFreeVars, rulesFreeVars,
@@ -35,10 +36,16 @@ module CoreFVs (
         expr_fvs,
 
         -- * Core syntax tree annotation with free variables
-        CoreExprWithFVs,        -- = AnnExpr Id DVarSet
-        CoreBindWithFVs,        -- = AnnBind Id DVarSet
+        FVAnn,                  -- annotation, abstract
+        CoreExprWithFVs,        -- = AnnExpr Id FVAnn
+        CoreExprWithFVs',       -- = AnnExpr' Id FVAnn
+        CoreBindWithFVs,        -- = AnnBind Id FVAnn
+        CoreAltWithFVs,         -- = AnnAlt Id FVAnn
         freeVars,               -- CoreExpr -> CoreExprWithFVs
-        freeVarsOf              -- CoreExprWithFVs -> DIdSet
+        freeVarsOf,             -- CoreExprWithFVs -> DIdSet
+        freeVarsOfType,         -- CoreExprWithFVs -> TyCoVarSet
+        freeVarsOfAnn, freeVarsOfTypeAnn,
+        exprTypeFV              -- CoreExprWithFVs -> Type
     ) where
 
 #include "HsVersions.h"
@@ -48,10 +55,12 @@ import Id
 import IdInfo
 import NameSet
 import UniqFM
+import Literal ( literalType )
 import Name
 import VarSet
 import Var
 import TcType
+import Type
 import Coercion
 import Maybes( orElse )
 import Util
@@ -161,7 +170,7 @@ exprsSomeFreeVars fv_cand es =
 
 addBndr :: CoreBndr -> FV -> FV
 addBndr bndr fv fv_cand in_scope acc
-  = (varTypeTyVarsAcc bndr `unionFV`
+  = (varTypeTyCoVarsAcc bndr `unionFV`
         -- Include type varibles in the binder's type
         --      (not just Ids; coercion variables too!)
      FV.delFV bndr fv) fv_cand in_scope acc
@@ -171,7 +180,7 @@ addBndrs bndrs fv = foldr addBndr fv bndrs
 
 expr_fvs :: CoreExpr -> FV
 expr_fvs (Type ty) fv_cand in_scope acc =
-  tyVarsOfTypeAcc ty fv_cand in_scope acc
+  tyCoVarsOfTypeAcc ty fv_cand in_scope acc
 expr_fvs (Coercion co) fv_cand in_scope acc =
   tyCoVarsOfCoAcc co fv_cand in_scope acc
 expr_fvs (Var var) fv_cand in_scope acc = oneVar var fv_cand in_scope acc
@@ -186,7 +195,7 @@ expr_fvs (Cast expr co) fv_cand in_scope acc =
   (expr_fvs expr `unionFV` tyCoVarsOfCoAcc co) fv_cand in_scope acc
 
 expr_fvs (Case scrut bndr ty alts) fv_cand in_scope acc
-  = (expr_fvs scrut `unionFV` tyVarsOfTypeAcc ty `unionFV` addBndr bndr
+  = (expr_fvs scrut `unionFV` tyCoVarsOfTypeAcc ty `unionFV` addBndr bndr
       (mapUnionFV alt_fvs alts)) fv_cand in_scope acc
   where
     alt_fvs (_, bndrs, rhs) = addBndrs bndrs (expr_fvs rhs)
@@ -353,16 +362,42 @@ The free variable pass annotates every node in the expression with its
 NON-GLOBAL free variables and type variables.
 -}
 
+data FVAnn = FVAnn { fva_fvs    :: DVarSet   -- free in expression
+                   , fva_ty_fvs :: DVarSet   -- free only in expression's type
+                   , fva_ty     :: Type      -- expression's type
+                   }
+
 -- | Every node in a binding group annotated with its
--- (non-global) free variables, both Ids and TyVars
-type CoreBindWithFVs = AnnBind Id DVarSet
+-- (non-global) free variables, both Ids and TyVars, and type.
+type CoreBindWithFVs = AnnBind Id FVAnn
+-- | Every node in an expression annotated with its
+-- (non-global) free variables, both Ids and TyVars, and type.
+type CoreExprWithFVs  = AnnExpr Id FVAnn
+type CoreExprWithFVs' = AnnExpr' Id FVAnn
+
 -- | Every node in an expression annotated with its
--- (non-global) free variables, both Ids and TyVars
-type CoreExprWithFVs = AnnExpr Id DVarSet
+-- (non-global) free variables, both Ids and TyVars, and type.
+type CoreAltWithFVs = AnnAlt Id FVAnn
 
 freeVarsOf :: CoreExprWithFVs -> DIdSet
 -- ^ Inverse function to 'freeVars'
-freeVarsOf (free_vars, _) = free_vars
+freeVarsOf (FVAnn { fva_fvs = fvs }, _) = fvs
+
+-- | Extract the vars free in an annotated expression's type
+freeVarsOfType :: CoreExprWithFVs -> DTyCoVarSet
+freeVarsOfType (FVAnn { fva_ty_fvs = ty_fvs }, _) = ty_fvs
+
+-- | Extract the type of an annotated expression. (This is cheap.)
+exprTypeFV :: CoreExprWithFVs -> Type
+exprTypeFV (FVAnn { fva_ty = ty }, _) = ty
+
+-- | Extract the vars reported in a FVAnn
+freeVarsOfAnn :: FVAnn -> DIdSet
+freeVarsOfAnn = fva_fvs
+
+-- | Extract the type-level vars reported in a FVAnn
+freeVarsOfTypeAnn :: FVAnn -> DTyCoVarSet
+freeVarsOfTypeAnn = fva_ty_fvs
 
 noFVs :: VarSet
 noFVs = emptyVarSet
@@ -373,6 +408,9 @@ aFreeVar = unitDVarSet
 unionFVs :: DVarSet -> DVarSet -> DVarSet
 unionFVs = unionDVarSet
 
+unionFVss :: [DVarSet] -> DVarSet
+unionFVss = unionDVarSets
+
 delBindersFV :: [Var] -> DVarSet -> DVarSet
 delBindersFV bs fvs = foldr delBinderFV fvs bs
 
@@ -407,27 +445,30 @@ delBinderFV :: Var -> DVarSet -> DVarSet
 --                        where
 --                          bottom = bottom -- Never evaluated
 
-delBinderFV b s = (s `delDVarSet` b) `unionFVs` dVarTypeTyVars b
+delBinderFV b s = (s `delDVarSet` b) `unionFVs` dVarTypeTyCoVars b
         -- Include coercion variables too!
 
-varTypeTyVars :: Var -> TyVarSet
+varTypeTyCoVars :: Var -> TyCoVarSet
 -- Find the type/kind variables free in the type of the id/tyvar
-varTypeTyVars var = runFVSet $ varTypeTyVarsAcc var
+varTypeTyCoVars var = runFVSet $ varTypeTyCoVarsAcc var
 
-dVarTypeTyVars :: Var -> DTyVarSet
--- Find the type/kind variables free in the type of the id/tyvar
-dVarTypeTyVars var = runFVDSet $ varTypeTyVarsAcc var
+dVarTypeTyCoVars :: Var -> DTyCoVarSet
+-- Find the type/kind/coercion variables free in the type of the id/tyvar
+dVarTypeTyCoVars var = runFVDSet $ varTypeTyCoVarsAcc var
 
-varTypeTyVarsAcc :: Var -> FV
-varTypeTyVarsAcc var = tyVarsOfTypeAcc (varType var)
+varTypeTyCoVarsAcc :: Var -> FV
+varTypeTyCoVarsAcc var = tyCoVarsOfTypeAcc (varType var)
 
 idFreeVars :: Id -> VarSet
 idFreeVars id = ASSERT( isId id) runFVSet $ idFreeVarsAcc id
 
+dIdFreeVars :: Id -> DVarSet
+dIdFreeVars id = runFVDSet $ idFreeVarsAcc id
+
 idFreeVarsAcc :: Id -> FV
 -- Type variables, rule variables, and inline variables
 idFreeVarsAcc id = ASSERT( isId id)
-                   varTypeTyVarsAcc id `unionFV`
+                   varTypeTyCoVarsAcc id `unionFV`
                    idRuleAndUnfoldingVarsAcc id
 
 bndrRuleAndUnfoldingVarsAcc :: Var -> FV
@@ -437,6 +478,9 @@ bndrRuleAndUnfoldingVarsAcc v | isTyVar v = noVars
 idRuleAndUnfoldingVars :: Id -> VarSet
 idRuleAndUnfoldingVars id = runFVSet $ idRuleAndUnfoldingVarsAcc id
 
+idRuleAndUnfoldingVarsDSet :: Id -> DVarSet
+idRuleAndUnfoldingVarsDSet id = runFVDSet $ idRuleAndUnfoldingVarsAcc id
+
 idRuleAndUnfoldingVarsAcc :: Id -> FV
 idRuleAndUnfoldingVarsAcc id = ASSERT( isId id)
                                idRuleVarsAcc id `unionFV` idUnfoldingVarsAcc id
@@ -485,83 +529,127 @@ stableUnfoldingVarsAcc unf
 
 freeVars :: CoreExpr -> CoreExprWithFVs
 -- ^ Annotate a 'CoreExpr' with its (non-global) free type and value variables at every tree node
-freeVars (Var v)
-  = (fvs, AnnVar v)
-  where
-        -- ToDo: insert motivating example for why we *need*
-        -- to include the idSpecVars in the FV list.
-        --      Actually [June 98] I don't think it's necessary
-        -- fvs = fvs_v `unionVarSet` idSpecVars v
-
-    fvs | isLocalVar v = aFreeVar v
-        | otherwise    = emptyDVarSet
-
-freeVars (Lit lit) = (emptyDVarSet, AnnLit lit)
-freeVars (Lam b body)
-  = (b `delBinderFV` freeVarsOf body', AnnLam b body')
-  where
-    body' = freeVars body
-
-freeVars (App fun arg)
-  = (freeVarsOf fun2 `unionFVs` freeVarsOf arg2, AnnApp fun2 arg2)
-  where
-    fun2 = freeVars fun
-    arg2 = freeVars arg
-
-freeVars (Case scrut bndr ty alts)
-  = ((bndr `delBinderFV` alts_fvs) `unionFVs` freeVarsOf scrut2 `unionFVs` runFVDSet (tyVarsOfTypeAcc ty),
-     AnnCase scrut2 bndr ty alts2)
+freeVars = go
   where
-    scrut2 = freeVars scrut
-
-    (alts_fvs_s, alts2) = mapAndUnzip fv_alt alts
-    alts_fvs            = foldr unionFVs emptyDVarSet alts_fvs_s
-
-    fv_alt (con,args,rhs) = (delBindersFV args (freeVarsOf rhs2),
-                             (con, args, rhs2))
-                          where
-                             rhs2 = freeVars rhs
-
-freeVars (Let (NonRec binder rhs) body)
-  = (freeVarsOf rhs2
-       `unionFVs` body_fvs
-       `unionFVs` runFVDSet (bndrRuleAndUnfoldingVarsAcc binder),
-                -- Remember any rules; cf rhs_fvs above
-     AnnLet (AnnNonRec binder rhs2) body2)
-  where
-    rhs2     = freeVars rhs
-    body2    = freeVars body
-    body_fvs = binder `delBinderFV` freeVarsOf body2
-
-freeVars (Let (Rec binds) body)
-  = (delBindersFV binders all_fvs,
-     AnnLet (AnnRec (binders `zip` rhss2)) body2)
-  where
-    (binders, rhss) = unzip binds
-
-    rhss2     = map freeVars rhss
-    rhs_body_fvs = foldr (unionFVs . freeVarsOf) body_fvs rhss2
-    binders_fvs = runFVDSet $ mapUnionFV idRuleAndUnfoldingVarsAcc binders
-    all_fvs      = rhs_body_fvs `unionFVs` binders_fvs
-        -- The "delBinderFV" happens after adding the idSpecVars,
-        -- since the latter may add some of the binders as fvs
-
-    body2     = freeVars body
-    body_fvs  = freeVarsOf body2
+    go :: CoreExpr -> CoreExprWithFVs
+    go (Var v)
+      = (FVAnn fvs ty_fvs (idType v), AnnVar v)
+      where
+            -- ToDo: insert motivating example for why we *need*
+            -- to include the idSpecVars in the FV list.
+            --      Actually [June 98] I don't think it's necessary
+            -- fvs = fvs_v `unionVarSet` idSpecVars v
+
+        (fvs, ty_fvs)
+            | isLocalVar v = (aFreeVar v `unionFVs` ty_fvs, dVarTypeTyCoVars v)
+            | otherwise    = (emptyDVarSet, emptyDVarSet)
+
+    go (Lit lit) = (FVAnn emptyDVarSet emptyDVarSet (literalType lit), AnnLit lit)
+    go (Lam b body)
+      = ( FVAnn { fva_fvs    = b_fvs `unionFVs` (b `delBinderFV` body_fvs)
+                , fva_ty_fvs = b_fvs `unionFVs` (b `delBinderFV` body_ty_fvs)
+                , fva_ty     = mkFunTy b_ty body_ty }
+        , AnnLam b body' )
+      where
+        body'@(FVAnn { fva_fvs = body_fvs, fva_ty_fvs = body_ty_fvs
+                     , fva_ty = body_ty }, _) = go body
+        b_ty  = idType b
+        b_fvs = tyCoVarsOfTypeDSet b_ty
+
+    go (App fun arg)
+      = ( FVAnn { fva_fvs    = freeVarsOf fun' `unionFVs` freeVarsOf arg'
+                , fva_ty_fvs = tyCoVarsOfTypeDSet res_ty
+                , fva_ty     = res_ty }
+        , AnnApp fun' arg' )
+      where
+        fun'   = go fun
+        fun_ty = exprTypeFV fun'
+        arg'   = go arg
+        res_ty = applyTypeToArg fun_ty arg
+
+    go (Case scrut bndr ty alts)
+      = ( FVAnn { fva_fvs = (bndr `delBinderFV` alts_fvs)
+                            `unionFVs` freeVarsOf scrut2
+                            `unionFVs` tyCoVarsOfTypeDSet ty
+                           -- don't need to look at (idType bndr)
+                           -- b/c that's redundant with scrut
+                , fva_ty_fvs = tyCoVarsOfTypeDSet ty
+                , fva_ty     = ty }
+        , AnnCase scrut2 bndr ty alts2 )
+      where
+        scrut2 = go scrut
+
+        (alts_fvs_s, alts2) = mapAndUnzip fv_alt alts
+        alts_fvs            = unionFVss alts_fvs_s
+
+        fv_alt (con,args,rhs) = (delBindersFV args (freeVarsOf rhs2),
+                                 (con, args, rhs2))
+                              where
+                                 rhs2 = go rhs
+
+    go (Let (NonRec binder rhs) body)
+      = ( FVAnn { fva_fvs    = freeVarsOf rhs2
+                               `unionFVs` body_fvs
+                               `unionFVs` runFVDSet
+                                            (bndrRuleAndUnfoldingVarsAcc binder)
+                               -- Remember any rules; cf rhs_fvs above
+                , fva_ty_fvs = freeVarsOfType body2
+                , fva_ty     = exprTypeFV body2 }
+        , AnnLet (AnnNonRec binder rhs2) body2 )
+      where
+        rhs2     = go rhs
+        body2    = go body
+        body_fvs = binder `delBinderFV` freeVarsOf body2
+
+    go (Let (Rec binds) body)
+      = ( FVAnn { fva_fvs    = delBindersFV binders all_fvs
+                , fva_ty_fvs = freeVarsOfType body2
+                , fva_ty     = exprTypeFV body2 }
+        , AnnLet (AnnRec (binders `zip` rhss2)) body2 )
+      where
+        (binders, rhss) = unzip binds
 
-freeVars (Cast expr co)
-  = (freeVarsOf expr2 `unionFVs` cfvs, AnnCast expr2 (cfvs, co))
-  where
-    expr2 = freeVars expr
-    cfvs  = runFVDSet $ tyCoVarsOfCoAcc co
+        rhss2        = map go rhss
+        rhs_body_fvs = foldr (unionFVs . freeVarsOf) body_fvs rhss2
+        binders_fvs  = runFVDSet $ mapUnionFV idRuleAndUnfoldingVarsAcc binders
+        all_fvs      = rhs_body_fvs `unionFVs` binders_fvs
+            -- The "delBinderFV" happens after adding the idSpecVars,
+            -- since the latter may add some of the binders as fvs
 
-freeVars (Tick tickish expr)
-  = (tickishFVs tickish `unionFVs` freeVarsOf expr2, AnnTick tickish expr2)
-  where
-    expr2 = freeVars expr
-    tickishFVs (Breakpoint _ ids) = mkDVarSet ids
-    tickishFVs _                  = emptyDVarSet
+        body2    = go body
+        body_fvs = freeVarsOf body2
 
-freeVars (Type ty) = (runFVDSet $ tyVarsOfTypeAcc ty, AnnType ty)
+    go (Cast expr co)
+      = ( FVAnn (freeVarsOf expr2 `unionFVs` cfvs) (tyCoVarsOfTypeDSet to_ty) to_ty
+        , AnnCast expr2 (c_ann, co) )
+      where
+        expr2 = go expr
+        cfvs  = tyCoVarsOfCoDSet co
+        c_ann = FVAnn cfvs (tyCoVarsOfTypeDSet co_ki) co_ki
+        co_ki = coercionType co
+        Just (_, to_ty) = splitCoercionType_maybe co_ki
+
+
+    go (Tick tickish expr)
+      = ( FVAnn { fva_fvs    = tickishFVs tickish `unionFVs` freeVarsOf expr2
+                , fva_ty_fvs = freeVarsOfType expr2
+                , fva_ty     = exprTypeFV expr2 }
+        , AnnTick tickish expr2 )
+      where
+        expr2 = go expr
+        tickishFVs (Breakpoint _ ids) = mkDVarSet ids
+        tickishFVs _                  = emptyDVarSet
+
+    go (Type ty) = ( FVAnn (tyCoVarsOfTypeDSet ty)
+                           (tyCoVarsOfTypeDSet ki)
+                           ki
+                   , AnnType ty)
+      where
+        ki = typeKind ty
 
-freeVars (Coercion co) = (runFVDSet $ tyCoVarsOfCoAcc co, AnnCoercion co)
+    go (Coercion co) = ( FVAnn (tyCoVarsOfCoDSet co)
+                               (tyCoVarsOfTypeDSet ki)
+                               ki
+                       , AnnCoercion co)
+      where
+        ki = coercionType co