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, 36 insertions, 37 deletions

diff --git a/compiler/main/GHC.hs b/compiler/main/GHC.hs
index 8e5a530700..965f7c1439 100644
--- a/compiler/main/GHC.hs
+++ b/compiler/main/GHC.hs
@@ -38,7 +38,7 @@ module GHC (
         addTarget,
         removeTarget,
         guessTarget,
-        
+
         -- * Loading\/compiling the program
         depanal,
         load, LoadHowMuch(..), InteractiveImport(..),
@@ -136,7 +136,7 @@ module GHC (
         SingleStep(..),
         Resume(resumeStmt, resumeThreadId, resumeBreakInfo, resumeSpan,
                resumeHistory, resumeHistoryIx),
-        History(historyBreakInfo, historyEnclosingDecls), 
+        History(historyBreakInfo, historyEnclosingDecls),
         GHC.getHistorySpan, getHistoryModule,
         abandon, abandonAll,
         getResumeContext,
@@ -164,11 +164,11 @@ module GHC (
         ModuleName, mkModuleName, moduleNameString,
 
         -- ** Names
-        Name, 
+        Name,
         isExternalName, nameModule, pprParenSymName, nameSrcSpan,
         NamedThing(..),
         RdrName(Qual,Unqual),
-        
+
         -- ** Identifiers
         Id, idType,
         isImplicitId, isDeadBinder,
@@ -186,7 +186,7 @@ module GHC (
         isPrimTyCon, isFunTyCon,
         isFamilyTyCon, isOpenFamilyTyCon, isOpenTypeFamilyTyCon,
         tyConClass_maybe,
-        synTyConRhs_maybe, synTyConDefn_maybe, tyConResKind,
+        synTyConRhs_maybe, synTyConDefn_maybe, tyConKind,
 
         -- ** Type variables
         TyVar,
@@ -200,46 +200,46 @@ module GHC (
         StrictnessMark(..), isMarkedStrict,
 
         -- ** Classes
-        Class, 
+        Class,
         classMethods, classSCTheta, classTvsFds, classATs,
         pprFundeps,
 
         -- ** Instances
-        ClsInst, 
-        instanceDFunId, 
+        ClsInst,
+        instanceDFunId,
         pprInstance, pprInstanceHdr,
         pprFamInst,
 
         FamInst,
 
         -- ** Types and Kinds
-        Type, splitForAllTys, funResultTy, 
-        pprParendType, pprTypeApp, 
+        Type, splitForAllTys, funResultTy,
+        pprParendType, pprTypeApp,
         Kind,
         PredType,
-        ThetaType, pprForAll, pprThetaArrowTy,
+        ThetaType, pprForAll, pprForAllImplicit, pprThetaArrowTy,
 
         -- ** Entities
-        TyThing(..), 
+        TyThing(..),
 
         -- ** Syntax
         module HsSyn, -- ToDo: remove extraneous bits
 
         -- ** Fixities
-        FixityDirection(..), 
-        defaultFixity, maxPrecedence, 
+        FixityDirection(..),
+        defaultFixity, maxPrecedence,
         negateFixity,
         compareFixity,
 
         -- ** Source locations
-        SrcLoc(..), RealSrcLoc, 
+        SrcLoc(..), RealSrcLoc,
         mkSrcLoc, noSrcLoc,
         srcLocFile, srcLocLine, srcLocCol,
         SrcSpan(..), RealSrcSpan,
         mkSrcSpan, srcLocSpan, isGoodSrcSpan, noSrcSpan,
         srcSpanStart, srcSpanEnd,
-        srcSpanFile, 
-        srcSpanStartLine, srcSpanEndLine, 
+        srcSpanFile,
+        srcSpanStartLine, srcSpanEndLine,
         srcSpanStartCol, srcSpanEndCol,
 
         -- ** Located
@@ -305,7 +305,6 @@ import NameSet
 import RdrName
 import HsSyn
 import Type     hiding( typeKind )
-import Kind             ( tyConResKind )
 import TcType           hiding( typeKind )
 import Id
 import TysPrim          ( alphaTyVars )
@@ -709,9 +708,9 @@ guessTarget str Nothing
         dflags <- getDynFlags
         liftIO $ throwGhcExceptionIO
                  (ProgramError (showSDoc dflags $
-                 text "target" <+> quotes (text file) <+> 
+                 text "target" <+> quotes (text file) <+>
                  text "is not a module name or a source file"))
-     where 
+     where
          (file,obj_allowed)
                 | '*':rest <- str = (rest, False)
                 | otherwise       = (str,  True)
@@ -724,7 +723,7 @@ guessTarget str Nothing
 
 -- | Inform GHC that the working directory has changed.  GHC will flush
 -- its cache of module locations, since it may no longer be valid.
--- 
+--
 -- Note: Before changing the working directory make sure all threads running
 -- in the same session have stopped.  If you change the working directory,
 -- you should also unload the current program (set targets to empty,
@@ -923,11 +922,11 @@ loadModule tcm = do
 
    mb_linkable <- case ms_obj_date ms of
                      Just t | t > ms_hs_date ms  -> do
-                         l <- liftIO $ findObjectLinkable (ms_mod ms) 
+                         l <- liftIO $ findObjectLinkable (ms_mod ms)
                                                   (ml_obj_file loc) t
                          return (Just l)
                      _otherwise -> return Nothing
-                                                
+
    let source_modified | isNothing mb_linkable = SourceModified
                        | otherwise             = SourceUnmodified
                        -- we can't determine stability here
@@ -1103,10 +1102,10 @@ getModuleInfo mdl = withSession $ \hsc_env -> do
 
 getPackageModuleInfo :: HscEnv -> Module -> IO (Maybe ModuleInfo)
 #ifdef GHCI
-getPackageModuleInfo hsc_env mdl 
+getPackageModuleInfo hsc_env mdl
   = do  eps <- hscEPS hsc_env
         iface <- hscGetModuleInterface hsc_env mdl
-        let 
+        let
             avails = mi_exports iface
             pte    = eps_PTE eps
             tys    = [ ty | name <- concatMap availNames avails,
@@ -1119,7 +1118,7 @@ getPackageModuleInfo hsc_env mdl
                         minf_instances = error "getModuleInfo: instances for package module unimplemented",
                         minf_iface     = Just iface,
                         minf_safe      = getSafeMode $ mi_trust iface,
-                        minf_modBreaks = emptyModBreaks  
+                        minf_modBreaks = emptyModBreaks
                 }))
 #else
 -- bogusly different for non-GHCI (ToDo)
@@ -1128,7 +1127,7 @@ getPackageModuleInfo _hsc_env _mdl = do
 #endif
 
 getHomeModuleInfo :: HscEnv -> Module -> IO (Maybe ModuleInfo)
-getHomeModuleInfo hsc_env mdl = 
+getHomeModuleInfo hsc_env mdl =
   case lookupUFM (hsc_HPT hsc_env) (moduleName mdl) of
     Nothing  -> return Nothing
     Just hmi -> do
@@ -1182,7 +1181,7 @@ modInfoLookupName minf name = withSession $ \hsc_env -> do
      Just tyThing -> return (Just tyThing)
      Nothing      -> do
        eps <- liftIO $ readIORef (hsc_EPS hsc_env)
-       return $! lookupType (hsc_dflags hsc_env) 
+       return $! lookupType (hsc_dflags hsc_env)
                             (hsc_HPT hsc_env) (eps_PTE eps) name
 
 modInfoIface :: ModuleInfo -> Maybe ModIface
@@ -1194,12 +1193,13 @@ modInfoSafe = minf_safe
 
 #ifdef GHCI
 modInfoModBreaks :: ModuleInfo -> ModBreaks
-modInfoModBreaks = minf_modBreaks  
+modInfoModBreaks = minf_modBreaks
 #endif
 
 isDictonaryId :: Id -> Bool
 isDictonaryId id
-  = case tcSplitSigmaTy (idType id) of { (_tvs, _theta, tau) -> isDictTy tau }
+  = case tcSplitSigmaTy (idType id) of {
+      (_tvs, _theta, tau) -> isDictTy tau }
 
 -- | Looks up a global name: that is, any top-level name in any
 -- visible module.  Unlike 'lookupName', lookupGlobalName does not use
@@ -1361,11 +1361,11 @@ showRichTokenStream ts = go startLoc ts ""
 -- Interactive evaluation
 
 -- | Takes a 'ModuleName' and possibly a 'UnitId', and consults the
--- filesystem and package database to find the corresponding 'Module', 
+-- filesystem and package database to find the corresponding 'Module',
 -- using the algorithm that is used for an @import@ declaration.
 findModule :: GhcMonad m => ModuleName -> Maybe FastString -> m Module
 findModule mod_name maybe_pkg = withSession $ \hsc_env -> do
-  let 
+  let
     dflags   = hsc_dflags hsc_env
     this_pkg = thisPackage dflags
   --
@@ -1388,7 +1388,7 @@ findModule mod_name maybe_pkg = withSession $ \hsc_env -> do
 
 modNotLoadedError :: DynFlags -> Module -> ModLocation -> IO a
 modNotLoadedError dflags m loc = throwGhcExceptionIO $ CmdLineError $ showSDoc dflags $
-   text "module is not loaded:" <+> 
+   text "module is not loaded:" <+>
    quotes (ppr (moduleName m)) <+>
    parens (text (expectJust "modNotLoadedError" (ml_hs_file loc)))
 
@@ -1465,7 +1465,7 @@ obtainTermFromId bound force id = withSession $ \hsc_env ->
 -- entity known to GHC, including 'Name's defined using 'runStmt'.
 lookupName :: GhcMonad m => Name -> m (Maybe TyThing)
 lookupName name =
-     withSession $ \hsc_env -> 
+     withSession $ \hsc_env ->
        liftIO $ hscTcRcLookupName hsc_env name
 
 -- -----------------------------------------------------------------------------
@@ -1478,17 +1478,16 @@ parser :: String         -- ^ Haskell module source text (full Unicode is suppor
        -> FilePath       -- ^ the filename (for source locations)
        -> Either ErrorMessages (WarningMessages, Located (HsModule RdrName))
 
-parser str dflags filename = 
+parser str dflags filename =
    let
        loc  = mkRealSrcLoc (mkFastString filename) 1 1
        buf  = stringToStringBuffer str
    in
    case unP Parser.parseModule (mkPState dflags buf loc) of
 
-     PFailed span err   -> 
+     PFailed span err   ->
          Left (unitBag (mkPlainErrMsg dflags span err))
 
      POk pst rdr_module ->
          let (warns,_) = getMessages pst in
          Right (warns, rdr_module)
-