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, 33 insertions, 26 deletions

diff --git a/compiler/ghci/RtClosureInspect.hs b/compiler/ghci/RtClosureInspect.hs
index 1ec127e35b..015126fae9 100644
--- a/compiler/ghci/RtClosureInspect.hs
+++ b/compiler/ghci/RtClosureInspect.hs
@@ -15,7 +15,7 @@ module RtClosureInspect(
      Term(..),
      isTerm, isSuspension, isPrim, isFun, isFunLike, isNewtypeWrap,
      isFullyEvaluated, isFullyEvaluatedTerm,
-     termType, mapTermType, termTyVars,
+     termType, mapTermType, termTyCoVars,
      foldTerm, TermFold(..), foldTermM, TermFoldM(..), idTermFold,
      pprTerm, cPprTerm, cPprTermBase, CustomTermPrinter,
 
@@ -311,14 +311,14 @@ mapTermTypeM f = foldTermM TermFoldM {
           fNewtypeWrapM= \ty dc t -> f ty >>= \ty' -> return $ NewtypeWrap ty' dc t,
           fRefWrapM    = \ty t -> f ty >>= \ty' -> return $ RefWrap ty' t}
 
-termTyVars :: Term -> TyVarSet
-termTyVars = foldTerm TermFold {
+termTyCoVars :: Term -> TyCoVarSet
+termTyCoVars = foldTerm TermFold {
             fTerm       = \ty _ _ tt   ->
-                          tyVarsOfType ty `plusVarEnv` concatVarEnv tt,
-            fSuspension = \_ ty _ _ -> tyVarsOfType ty,
+                          tyCoVarsOfType ty `plusVarEnv` concatVarEnv tt,
+            fSuspension = \_ ty _ _ -> tyCoVarsOfType ty,
             fPrim       = \ _ _ -> emptyVarEnv,
-            fNewtypeWrap= \ty _ t -> tyVarsOfType ty `plusVarEnv` t,
-            fRefWrap    = \ty t -> tyVarsOfType ty `plusVarEnv` t}
+            fNewtypeWrap= \ty _ t -> tyCoVarsOfType ty `plusVarEnv` t,
+            fRefWrap    = \ty t -> tyCoVarsOfType ty `plusVarEnv` t}
     where concatVarEnv = foldr plusVarEnv emptyVarEnv
 
 ----------------------------------
@@ -599,10 +599,14 @@ liftTcM = id
 newVar :: Kind -> TR TcType
 newVar = liftTcM . newFlexiTyVarTy
 
-instTyVars :: [TyVar] -> TR (TvSubst, [TcTyVar])
+newOpenVar :: TR TcType
+newOpenVar = liftTcM newOpenFlexiTyVarTy
+
+instTyVars :: [TyVar] -> TR (TCvSubst, [TcTyVar])
 -- Instantiate fresh mutable type variables from some TyVars
 -- This function preserves the print-name, which helps error messages
-instTyVars = liftTcM . tcInstTyVars
+instTyVars tvs
+  = liftTcM $ fst <$> captureConstraints (tcInstTyVars tvs)
 
 type RttiInstantiation = [(TcTyVar, TyVar)]
    -- Associates the typechecker-world meta type variables
@@ -616,9 +620,9 @@ type RttiInstantiation = [(TcTyVar, TyVar)]
 --   mapping from new (instantiated) -to- old (skolem) type variables
 instScheme :: QuantifiedType -> TR (TcType, RttiInstantiation)
 instScheme (tvs, ty)
-  = liftTcM $ do { (subst, tvs') <- tcInstTyVars tvs
-                 ; let rtti_inst = [(tv',tv) | (tv',tv) <- tvs' `zip` tvs]
-                 ; return (substTy subst ty, rtti_inst) }
+  = do { (subst, tvs') <- instTyVars tvs
+       ; let rtti_inst = [(tv',tv) | (tv',tv) <- tvs' `zip` tvs]
+       ; return (substTy subst ty, rtti_inst) }
 
 applyRevSubst :: RttiInstantiation -> TR ()
 -- Apply the *reverse* substitution in-place to any un-filled-in
@@ -642,13 +646,13 @@ addConstraint actual expected = do
     traceTR (text "add constraint:" <+> fsep [ppr actual, equals, ppr expected])
     recoverTR (traceTR $ fsep [text "Failed to unify", ppr actual,
                                     text "with", ppr expected]) $
+      discardResult $
+      captureConstraints $
       do { (ty1, ty2) <- congruenceNewtypes actual expected
-         ; _  <- captureConstraints $ unifyType ty1 ty2
-         ; return () }
+         ; unifyType noThing ty1 ty2 }
      -- TOMDO: what about the coercion?
      -- we should consider family instances
 
-
 -- Type & Term reconstruction
 ------------------------------
 cvObtainTerm :: HscEnv -> Int -> Bool -> RttiType -> HValue -> IO Term
@@ -657,7 +661,7 @@ cvObtainTerm hsc_env max_depth force old_ty hval = runTR hsc_env $ do
   -- as this is needed to be able to manipulate
   -- them properly
    let quant_old_ty@(old_tvs, old_tau) = quantifyType old_ty
-       sigma_old_ty = mkForAllTys old_tvs old_tau
+       sigma_old_ty = mkInvForAllTys old_tvs old_tau
    traceTR (text "Term reconstruction started with initial type " <> ppr old_ty)
    term <-
      if null old_tvs
@@ -667,7 +671,7 @@ cvObtainTerm hsc_env max_depth force old_ty hval = runTR hsc_env $ do
         return $ fixFunDictionaries $ expandNewtypes term'
       else do
               (old_ty', rev_subst) <- instScheme quant_old_ty
-              my_ty <- newVar openTypeKind
+              my_ty <- newOpenVar
               when (check1 quant_old_ty) (traceTR (text "check1 passed") >>
                                           addConstraint my_ty old_ty')
               term  <- go max_depth my_ty sigma_old_ty hval
@@ -687,7 +691,7 @@ cvObtainTerm hsc_env max_depth force old_ty hval = runTR hsc_env $ do
                       zterm' <- mapTermTypeM
                                  (\ty -> case tcSplitTyConApp_maybe ty of
                                            Just (tc, _:_) | tc /= funTyCon
-                                               -> newVar openTypeKind
+                                               -> newOpenVar
                                            _   -> return ty)
                                  term
                       zonkTerm zterm'
@@ -797,13 +801,14 @@ cvObtainTerm hsc_env max_depth force old_ty hval = runTR hsc_env $ do
 
 extractSubTerms :: (Type -> HValue -> TcM Term)
                 -> Closure -> [Type] -> TcM [Term]
-extractSubTerms recurse clos = liftM thirdOf3 . go 0 (nonPtrs clos)
+extractSubTerms recurse clos = liftM thdOf3 . go 0 (nonPtrs clos)
   where
     go ptr_i ws [] = return (ptr_i, ws, [])
     go ptr_i ws (ty:tys)
       | Just (tc, elem_tys) <- tcSplitTyConApp_maybe ty
       , isUnboxedTupleTyCon tc
-      = do (ptr_i, ws, terms0) <- go ptr_i ws elem_tys
+                -- See Note [Unboxed tuple levity vars] in TyCon
+      = do (ptr_i, ws, terms0) <- go ptr_i ws (drop (length elem_tys `div` 2) elem_tys)
            (ptr_i, ws, terms1) <- go ptr_i ws tys
            return (ptr_i, ws, unboxedTupleTerm ty terms0 : terms1)
       | otherwise
@@ -849,7 +854,7 @@ cvReconstructType hsc_env max_depth old_ty hval = runTR_maybe hsc_env $ do
         then return old_ty
         else do
           (old_ty', rev_subst) <- instScheme sigma_old_ty
-          my_ty <- newVar openTypeKind
+          my_ty <- newOpenVar
           when (check1 sigma_old_ty) (traceTR (text "check1 passed") >>
                                       addConstraint my_ty old_ty')
           search (isMonomorphic `fmap` zonkTcType my_ty)
@@ -941,7 +946,7 @@ findPtrTyss i tys = foldM step (i, []) tys
 -- improveType <base_type> <rtti_type>
 -- The types can contain skolem type variables, which need to be treated as normal vars.
 -- In particular, we want them to unify with things.
-improveRTTIType :: HscEnv -> RttiType -> RttiType -> Maybe TvSubst
+improveRTTIType :: HscEnv -> RttiType -> RttiType -> Maybe TCvSubst
 improveRTTIType _ base_ty new_ty = U.tcUnifyTy base_ty new_ty
 
 getDataConArgTys :: DataCon -> Type -> TR [Type]
@@ -1109,7 +1114,7 @@ If that is not the case, then we consider two conditions.
 check1 :: QuantifiedType -> Bool
 check1 (tvs, _) = not $ any isHigherKind (map tyVarKind tvs)
  where
-   isHigherKind = not . null . fst . splitKindFunTys
+   isHigherKind = not . null . fst . splitPiTys
 
 check2 :: QuantifiedType -> QuantifiedType -> Bool
 check2 (_, rtti_ty) (_, old_ty)
@@ -1191,7 +1196,7 @@ congruenceNewtypes lhs rhs = go lhs rhs >>= \rhs' -> return (lhs,rhs')
                (_, vars) <- instTyVars (tyConTyVars new_tycon)
                let ty' = mkTyConApp new_tycon (mkTyVarTys vars)
                    UnaryRep rep_ty = repType ty'
-               _ <- liftTcM (unifyType ty rep_ty)
+               _ <- liftTcM (unifyType noThing ty rep_ty)
         -- assumes that reptype doesn't ^^^^ touch tyconApp args
                return ty'
 
@@ -1232,7 +1237,7 @@ dictsView ty = ty
 isMonomorphic :: RttiType -> Bool
 isMonomorphic ty = noExistentials && noUniversals
  where (tvs, _, ty')  = tcSplitSigmaTy ty
-       noExistentials = isEmptyVarSet (tyVarsOfType ty')
+       noExistentials = isEmptyVarSet (tyCoVarsOfType ty')
        noUniversals   = null tvs
 
 -- Use only for RTTI types
@@ -1268,7 +1273,9 @@ quantifyType :: Type -> QuantifiedType
 -- Thus (quantifyType (forall a. a->[b]))
 -- returns ([a,b], a -> [b])
 
-quantifyType ty = (tyVarsOfTypeList rho, rho)
+quantifyType ty = ( filter isTyVar $
+                    tyCoVarsOfTypeWellScoped rho
+                  , rho)
   where
     (_tvs, rho) = tcSplitForAllTys ty