Type vs Constraint: finally nailed

This big patch addresses the rats-nest of issues that have plagued
us for years, about the relationship between Type and Constraint.
See #11715/#21623.

The main payload of the patch is:
* To introduce CONSTRAINT :: RuntimeRep -> Type
* To make TYPE and CONSTRAINT distinct throughout the compiler

Two overview Notes in GHC.Builtin.Types.Prim

* Note [TYPE and CONSTRAINT]

* Note [Type and Constraint are not apart]
  This is the main complication.

The specifics

* New primitive types (GHC.Builtin.Types.Prim)
  - CONSTRAINT
  - ctArrowTyCon (=>)
  - tcArrowTyCon (-=>)
  - ccArrowTyCon (==>)
  - funTyCon     FUN     -- Not new
  See Note [Function type constructors and FunTy]
  and Note [TYPE and CONSTRAINT]

* GHC.Builtin.Types:
  - New type Constraint = CONSTRAINT LiftedRep
  - I also stopped nonEmptyTyCon being built-in; it only needs to be wired-in

* Exploit the fact that Type and Constraint are distinct throughout GHC
  - Get rid of tcView in favour of coreView.
  - Many tcXX functions become XX functions.
    e.g. tcGetCastedTyVar --> getCastedTyVar

* Kill off Note [ForAllTy and typechecker equality], in (old)
  GHC.Tc.Solver.Canonical.  It said that typechecker-equality should ignore
  the specified/inferred distinction when comparein two ForAllTys.  But
  that wsa only weakly supported and (worse) implies that we need a separate
  typechecker equality, different from core equality. No no no.

* GHC.Core.TyCon: kill off FunTyCon in data TyCon.  There was no need for it,
  and anyway now we have four of them!

* GHC.Core.TyCo.Rep: add two FunTyFlags to FunCo
  See Note [FunCo] in that module.

* GHC.Core.Type.  Lots and lots of changes driven by adding CONSTRAINT.
  The key new function is sORTKind_maybe; most other changes are built
  on top of that.

  See also `funTyConAppTy_maybe` and `tyConAppFun_maybe`.

* Fix a longstanding bug in GHC.Core.Type.typeKind, and Core Lint, in
  kinding ForAllTys.  See new tules (FORALL1) and (FORALL2) in GHC.Core.Type.
  (The bug was that before (forall (cv::t1 ~# t2). blah), where
  blah::TYPE IntRep, would get kind (TYPE IntRep), but it should be
  (TYPE LiftedRep).  See Note [Kinding rules for types] in GHC.Core.Type.

* GHC.Core.TyCo.Compare is a new module in which we do eqType and cmpType.
  Of course, no tcEqType any more.

* GHC.Core.TyCo.FVs. I moved some free-var-like function into this module:
  tyConsOfType, visVarsOfType, and occCheckExpand.  Refactoring only.

* GHC.Builtin.Types.  Compiletely re-engineer boxingDataCon_maybe to
  have one for each /RuntimeRep/, rather than one for each /Type/.
  This dramatically widens the range of types we can auto-box.
  See Note [Boxing constructors] in GHC.Builtin.Types
  The boxing types themselves are declared in library ghc-prim:GHC.Types.

  GHC.Core.Make.  Re-engineer the treatment of "big" tuples (mkBigCoreVarTup
  etc) GHC.Core.Make, so that it auto-boxes unboxed values and (crucially)
  types of kind Constraint. That allows the desugaring for arrows to work;
  it gathers up free variables (including dictionaries) into tuples.
  See  Note [Big tuples] in GHC.Core.Make.

  There is still work to do here: #22336. But things are better than
  before.

* GHC.Core.Make.  We need two absent-error Ids, aBSENT_ERROR_ID for types of
  kind Type, and aBSENT_CONSTRAINT_ERROR_ID for vaues of kind Constraint.
  Ditto noInlineId vs noInlieConstraintId in GHC.Types.Id.Make;
  see Note [inlineId magic].

* GHC.Core.TyCo.Rep. Completely refactor the NthCo coercion.  It is now called
  SelCo, and its fields are much more descriptive than the single Int we used to
  have.  A great improvement.  See Note [SelCo] in GHC.Core.TyCo.Rep.

* GHC.Core.RoughMap.roughMatchTyConName.  Collapse TYPE and CONSTRAINT to
  a single TyCon, so that the rough-map does not distinguish them.

* GHC.Core.DataCon
  - Mainly just improve documentation

* Some significant renamings:
  GHC.Core.Multiplicity: Many -->  ManyTy (easier to grep for)
                         One  -->  OneTy
  GHC.Core.TyCo.Rep TyCoBinder      -->   GHC.Core.Var.PiTyBinder
  GHC.Core.Var      TyCoVarBinder   -->   ForAllTyBinder
                    AnonArgFlag     -->   FunTyFlag
                    ArgFlag         -->   ForAllTyFlag
  GHC.Core.TyCon    TyConTyCoBinder --> TyConPiTyBinder
  Many functions are renamed in consequence
  e.g. isinvisibleArgFlag becomes isInvisibleForAllTyFlag, etc

* I refactored FunTyFlag (was AnonArgFlag) into a simple, flat data type
    data FunTyFlag
      = FTF_T_T           -- (->)  Type -> Type
      | FTF_T_C           -- (-=>) Type -> Constraint
      | FTF_C_T           -- (=>)  Constraint -> Type
      | FTF_C_C           -- (==>) Constraint -> Constraint

* GHC.Tc.Errors.Ppr.  Some significant refactoring in the TypeEqMisMatch case
  of pprMismatchMsg.

* I made the tyConUnique field of TyCon strict, because I
  saw code with lots of silly eval's.  That revealed that
  GHC.Settings.Constants.mAX_SUM_SIZE can only be 63, because
  we pack the sum tag into a 6-bit field.  (Lurking bug squashed.)

Fixes
* #21530

Updates haddock submodule slightly.

Performance changes
~~~~~~~~~~~~~~~~~~~
I was worried that compile times would get worse, but after
some careful profiling we are down to a geometric mean 0.1%
increase in allocation (in perf/compiler).  That seems fine.

There is a big runtime improvement in T10359

Metric Decrease:
    LargeRecord
    MultiLayerModulesTH_OneShot
    T13386
    T13719
Metric Increase:
    T8095

2 files changed, 26 insertions, 66 deletions

diff --git a/compiler/GHC/Core/Map/Expr.hs b/compiler/GHC/Core/Map/Expr.hs
index 61fca8353a..96eefd65e9 100644
--- a/compiler/GHC/Core/Map/Expr.hs
+++ b/compiler/GHC/Core/Map/Expr.hs
@@ -150,9 +150,8 @@ instance Eq (DeBruijn CoreExpr) where
 
 eqDeBruijnExpr :: DeBruijn CoreExpr -> DeBruijn CoreExpr -> Bool
 eqDeBruijnExpr (D env1 e1) (D env2 e2) = go e1 e2 where
-    go (Var v1) (Var v2) = eqDeBruijnVar (D env1 v1) (D env2 v2)
+    go (Var v1) (Var v2)             = eqDeBruijnVar (D env1 v1) (D env2 v2)
     go (Lit lit1)    (Lit lit2)      = lit1 == lit2
-    -- See Note [Using tcView inside eqDeBruijnType] in GHC.Core.Map.Type
     go (Type t1)    (Type t2)        = eqDeBruijnType (D env1 t1) (D env2 t2)
     -- See Note [Alpha-equality for Coercion arguments]
     go (Coercion {}) (Coercion {}) = True
@@ -163,7 +162,6 @@ eqDeBruijnExpr (D env1 e1) (D env2 e2) = go e1 e2 where
       && go e1 e2
 
     go (Lam b1 e1)  (Lam b2 e2)
-          -- See Note [Using tcView inside eqDeBruijnType] in GHC.Core.Map.Type
       =  eqDeBruijnType (D env1 (varType b1)) (D env2 (varType b2))
       && D env1 (varMultMaybe b1) == D env2 (varMultMaybe b2)
       && eqDeBruijnExpr (D (extendCME env1 b1) e1) (D (extendCME env2 b2) e2)
@@ -175,9 +173,7 @@ eqDeBruijnExpr (D env1 e1) (D env2 e2) = go e1 e2 where
     go (Let (Rec ps1) e1) (Let (Rec ps2) e2)
       = equalLength ps1 ps2
       -- See Note [Alpha-equality for let-bindings]
-      && all2 (\b1 b2 -> -- See Note [Using tcView inside eqDeBruijnType] in
-                         -- GHC.Core.Map.Type
-                         eqDeBruijnType (D env1 (varType b1))
+      && all2 (\b1 b2 -> eqDeBruijnType (D env1 (varType b1))
                                         (D env2 (varType b2)))
               bs1 bs2
       && D env1' rs1 == D env2' rs2
diff --git a/compiler/GHC/Core/Map/Type.hs b/compiler/GHC/Core/Map/Type.hs
index 45468e654f..e57222075a 100644
--- a/compiler/GHC/Core/Map/Type.hs
+++ b/compiler/GHC/Core/Map/Type.hs
@@ -38,6 +38,7 @@ import GHC.Prelude
 import GHC.Core.Type
 import GHC.Core.Coercion
 import GHC.Core.TyCo.Rep
+import GHC.Core.TyCo.Compare( eqForAllVis )
 import GHC.Data.TrieMap
 
 import GHC.Data.FastString
@@ -54,7 +55,6 @@ import qualified Data.Map    as Map
 import qualified Data.IntMap as IntMap
 
 import Control.Monad ( (>=>) )
-import GHC.Data.Maybe
 
 -- NB: Be careful about RULES and type families (#5821).  So we should make sure
 -- to specify @Key TypeMapX@ (and not @DeBruijn Type@, the reduced form)
@@ -149,13 +149,6 @@ data TypeMapX a
   = TM { tm_var    :: VarMap a
        , tm_app    :: TypeMapG (TypeMapG a)  -- Note [Equality on AppTys] in GHC.Core.Type
        , tm_tycon  :: DNameEnv a
-
-         -- only InvisArg arrows here
-       , tm_funty  :: TypeMapG (TypeMapG (TypeMapG a))
-                       -- keyed on the argument, result rep, and result
-                       -- constraints are never linear-restricted and are always lifted
-                       -- See also Note [Equality on FunTys] in GHC.Core.TyCo.Rep
-
        , tm_forall :: TypeMapG (BndrMap a) -- See Note [Binders] in GHC.Core.Map.Expr
        , tm_tylit  :: TyLitMap a
        , tm_coerce :: Maybe a
@@ -165,28 +158,27 @@ data TypeMapX a
 -- | Squeeze out any synonyms, and change TyConApps to nested AppTys. Why the
 -- last one? See Note [Equality on AppTys] in GHC.Core.Type
 --
--- Note, however, that we keep Constraint and Type apart here, despite the fact
--- that they are both synonyms of TYPE 'LiftedRep (see #11715).
---
 -- We also keep (Eq a => a) as a FunTy, distinct from ((->) (Eq a) a).
 trieMapView :: Type -> Maybe Type
 trieMapView ty
   -- First check for TyConApps that need to be expanded to
-  -- AppTy chains.
-  | Just (tc, tys@(_:_)) <- tcSplitTyConApp_maybe ty
+  -- AppTy chains.  This includes eliminating FunTy entirely.
+  | Just (tc, tys@(_:_)) <- splitTyConApp_maybe ty
   = Just $ foldl' AppTy (mkTyConTy tc) tys
 
   -- Then resolve any remaining nullary synonyms.
-  | Just ty' <- tcView ty = Just ty'
+  | Just ty' <- coreView ty
+  = Just ty'
+
 trieMapView _ = Nothing
 
 -- TODO(22292): derive
 instance Functor TypeMapX where
     fmap f TM
-      { tm_var = tvar, tm_app = tapp, tm_tycon = ttycon, tm_funty = tfunty, tm_forall = tforall
+      { tm_var = tvar, tm_app = tapp, tm_tycon = ttycon, tm_forall = tforall
       , tm_tylit = tlit, tm_coerce = tcoerce } = TM
       { tm_var = fmap f tvar, tm_app = fmap (fmap f) tapp, tm_tycon = fmap f ttycon
-      , tm_funty = fmap (fmap (fmap f)) tfunty, tm_forall = fmap (fmap f) tforall
+      , tm_forall = fmap (fmap f) tforall
       , tm_tylit  = fmap f tlit, tm_coerce = fmap f tcoerce }
 
 instance TrieMap TypeMapX where
@@ -200,27 +192,6 @@ instance TrieMap TypeMapX where
 instance Eq (DeBruijn Type) where
   (==) = eqDeBruijnType
 
-{- Note [Using tcView inside eqDeBruijnType]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-`eqDeBruijnType` uses `tcView` and thus treats Type and Constraint as
-distinct -- see Note [coreView vs tcView] in GHC.Core.Type. We do that because
-`eqDeBruijnType` is used in TrieMaps, which are used for instance for instance
-selection in the type checker. [Or at least will be soon.]
-
-However, the odds that we have two expressions that are identical save for the
-'Type'/'Constraint' distinction are low. (Not impossible to do. But doubtful
-anyone has ever done so in the history of Haskell.)
-
-And it's actually all OK: 'eqCoreExpr' is conservative: if `eqCoreExpr e1 e2` returns
-'True', thne it must be that `e1` behaves identically to `e2` in all contexts.
-But if `eqCoreExpr e1 e2` returns 'False', then we learn nothing. The use of
-'tcView' where we expect 'coreView' means 'eqCoreExpr' returns 'False' bit more
-often that it should. This might, say, stop a `RULE` from firing or CSE from
-optimizing an expression. Stopping `RULE` firing is good actually: `RULES` are
-written in Haskell, where `Type /= Constraint`. Stopping CSE is unfortunate,
-but tolerable.
--}
-
 -- | An equality relation between two 'Type's (known below as @t1 :: k2@
 -- and @t2 :: k2@)
 data TypeEquality = TNEQ -- ^ @t1 /= t2@
@@ -262,9 +233,8 @@ eqDeBruijnType env_t1@(D env1 t1) env_t2@(D env2 t2) =
       | tc1 == tc2
       = TEQ
     go env_t@(D env t) env_t'@(D env' t')
-      -- See Note [Using tcView inside eqDeBruijnType]
-      | Just new_t  <- tcView t  = go (D env new_t) env_t'
-      | Just new_t' <- tcView t' = go env_t (D env' new_t')
+      | Just new_t  <- coreView t  = go (D env new_t) env_t'
+      | Just new_t' <- coreView t' = go env_t (D env' new_t')
       | otherwise
       = case (t, t') of
           -- See Note [Non-trivial definitional equality] in GHC.Core.TyCo.Rep
@@ -274,9 +244,9 @@ eqDeBruijnType env_t1@(D env1 t1) env_t2@(D env2 t2) =
           (TyVarTy v, TyVarTy v')
               -> liftEquality $ eqDeBruijnVar (D env v) (D env' v')
           -- See Note [Equality on AppTys] in GHC.Core.Type
-          (AppTy t1 t2, s) | Just (t1', t2') <- repSplitAppTy_maybe s
+          (AppTy t1 t2, s) | Just (t1', t2') <- splitAppTyNoView_maybe s
               -> go (D env t1) (D env' t1') `andEq` go (D env t2) (D env' t2')
-          (s, AppTy t1' t2') | Just (t1, t2) <- repSplitAppTy_maybe s
+          (s, AppTy t1' t2') | Just (t1, t2) <- splitAppTyNoView_maybe s
               -> go (D env t1) (D env' t1') `andEq` go (D env t2) (D env' t2')
           (FunTy v1 w1 t1 t2, FunTy v1' w1' t1' t2')
 
@@ -292,9 +262,9 @@ eqDeBruijnType env_t1@(D env1 t1) env_t2@(D env2 t2) =
           (LitTy l, LitTy l')
               -> liftEquality (l == l')
           (ForAllTy (Bndr tv vis) ty, ForAllTy (Bndr tv' vis') ty')
-              -> -- See Note [ForAllTy and typechecker equality] in
-                 -- GHC.Tc.Solver.Canonical for why we use `sameVis` here
-                 liftEquality (vis `sameVis` vis') `andEq`
+              -> -- See Note [ForAllTy and type equality] in
+                 -- GHC.Core.TyCo.Compare for why we use `eqForAllVis` here
+                 liftEquality (vis `eqForAllVis` vis') `andEq`
                  go (D env (varType tv)) (D env' (varType tv')) `andEq`
                  go (D (extendCME env tv) ty) (D (extendCME env' tv') ty')
           (CoercionTy {}, CoercionTy {})
@@ -324,7 +294,6 @@ emptyT :: TypeMapX a
 emptyT = TM { tm_var  = emptyTM
             , tm_app  = emptyTM
             , tm_tycon  = emptyDNameEnv
-            , tm_funty  = emptyTM
             , tm_forall = emptyTM
             , tm_tylit  = emptyTyLitMap
             , tm_coerce = Nothing }
@@ -338,19 +307,17 @@ lkT (D env ty) m = go ty m
     go (AppTy t1 t2)               = tm_app    >.> lkG (D env t1)
                                                >=> lkG (D env t2)
     go (TyConApp tc [])            = tm_tycon  >.> lkDNamed tc
-    go ty@(TyConApp _ (_:_))       = pprPanic "lkT TyConApp" (ppr ty)
     go (LitTy l)                   = tm_tylit  >.> lkTyLit l
     go (ForAllTy (Bndr tv _) ty)   = tm_forall >.> lkG (D (extendCME env tv) ty)
                                                >=> lkBndr env tv
-    go (FunTy InvisArg _ arg res)
-      | Just res_rep <- getRuntimeRep_maybe res
-                                   = tm_funty >.> lkG (D env arg)
-                                              >=> lkG (D env res_rep)
-                                              >=> lkG (D env res)
-    go ty@(FunTy {})               = pprPanic "lkT FunTy" (ppr ty)
     go (CastTy t _)                = go t
     go (CoercionTy {})             = tm_coerce
 
+    -- trieMapView has eliminated non-nullary TyConApp
+    -- and FunTy into an AppTy chain
+    go ty@(TyConApp _ (_:_))       = pprPanic "lkT TyConApp" (ppr ty)
+    go ty@(FunTy {})               = pprPanic "lkT FunTy" (ppr ty)
+
 -----------------
 xtT :: DeBruijn Type -> XT a -> TypeMapX a -> TypeMapX a
 xtT (D env ty) f m | Just ty' <- trieMapView ty = xtT (D env ty') f m
@@ -359,16 +326,15 @@ xtT (D env (TyVarTy v))       f m = m { tm_var    = tm_var m |> xtVar env v f }
 xtT (D env (AppTy t1 t2))     f m = m { tm_app    = tm_app m |> xtG (D env t1)
                                                             |>> xtG (D env t2) f }
 xtT (D _   (TyConApp tc []))  f m = m { tm_tycon  = tm_tycon m |> xtDNamed tc f }
-xtT (D env (FunTy InvisArg _ t1 t2)) f m = m { tm_funty = tm_funty m |> xtG (D env t1)
-                                                                    |>> xtG (D env t2_rep)
-                                                                    |>> xtG (D env t2) f }
-  where t2_rep = expectJust "xtT FunTy InvisArg" (getRuntimeRep_maybe t2)
 xtT (D _   (LitTy l))         f m = m { tm_tylit  = tm_tylit m |> xtTyLit l f }
 xtT (D env (CastTy t _))      f m = xtT (D env t) f m
 xtT (D _   (CoercionTy {}))   f m = m { tm_coerce = tm_coerce m |> f }
 xtT (D env (ForAllTy (Bndr tv _) ty))  f m
   = m { tm_forall = tm_forall m |> xtG (D (extendCME env tv) ty)
                                 |>> xtBndr env tv f }
+
+-- trieMapView has eliminated non-nullary TyConApp
+-- and FunTy into an AppTy chain
 xtT (D _   ty@(TyConApp _ (_:_))) _ _ = pprPanic "xtT TyConApp" (ppr ty)
 xtT (D _   ty@(FunTy {}))         _ _ = pprPanic "xtT FunTy" (ppr ty)
 
@@ -376,19 +342,17 @@ fdT :: (a -> b -> b) -> TypeMapX a -> b -> b
 fdT k m = foldTM k (tm_var m)
         . foldTM (foldTM k) (tm_app m)
         . foldTM k (tm_tycon m)
-        . foldTM (foldTM (foldTM k)) (tm_funty m)
         . foldTM (foldTM k) (tm_forall m)
         . foldTyLit k (tm_tylit m)
         . foldMaybe k (tm_coerce m)
 
 filterT :: (a -> Bool) -> TypeMapX a -> TypeMapX a
 filterT f (TM { tm_var  = tvar, tm_app = tapp, tm_tycon = ttycon
-              , tm_funty = tfunty, tm_forall = tforall, tm_tylit = tlit
+              , tm_forall = tforall, tm_tylit = tlit
               , tm_coerce = tcoerce })
   = TM { tm_var    = filterTM f tvar
        , tm_app    = fmap (filterTM f) tapp
        , tm_tycon  = filterTM f ttycon
-       , tm_funty  = fmap (fmap (filterTM f)) tfunty
        , tm_forall = fmap (filterTM f) tforall
        , tm_tylit  = filterTM f tlit
        , tm_coerce = filterMaybe f tcoerce }