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

4 files changed, 71 insertions, 11 deletions

diff --git a/libraries/base/Data/Typeable/Internal.hs b/libraries/base/Data/Typeable/Internal.hs
index 9bcc23daf5..209324d585 100644
--- a/libraries/base/Data/Typeable/Internal.hs
+++ b/libraries/base/Data/Typeable/Internal.hs
@@ -182,8 +182,9 @@ rnfTyCon (TyCon _ _ m n _ k) = rnfModule m `seq` rnfTrName n `seq` rnfKindRep k
 *                                                                      *
 ********************************************************************* -}
 
--- | A concrete representation of a (monomorphic) type.
+-- | TypeRep is a concrete representation of a (monomorphic) type.
 -- 'TypeRep' supports reasonably efficient equality.
+-- See Note [Grand plan for Typeable] in GHC.Tc.Instance.Typeable
 type TypeRep :: k -> Type
 data TypeRep a where
     -- The TypeRep of Type. See Note [Kind caching], Wrinkle 2
@@ -216,6 +217,11 @@ data TypeRep a where
 
     -- | @TrFun fpr m a b@ represents a function type @a % m -> b@. We use this for
     -- the sake of efficiency as functions are quite ubiquitous.
+    -- A TrFun can represent `t1 -> t2` or `t1 -= t2`; but not  (a => b) or (a ==> b).
+    -- See Note [No Typeable for polytypes or qualified types] in GHC.Tc.Instance.Class
+    -- and Note [Function type constructors and FunTy] in GHC.Builtin.Types.Prim
+    -- We do not represent the function TyCon (i.e. (->) vs (-=>)) explicitly;
+    -- instead, the TyCon is implicit in the kinds of the arguments.
     TrFun   :: forall (m :: Multiplicity) (r1 :: RuntimeRep) (r2 :: RuntimeRep)
                       (a :: TYPE r1) (b :: TYPE r2).
                { -- See Note [TypeRep fingerprints]
diff --git a/libraries/ghc-prim/GHC/Magic/Dict.hs b/libraries/ghc-prim/GHC/Magic/Dict.hs
index 34886fee3b..96820a502c 100644
--- a/libraries/ghc-prim/GHC/Magic/Dict.hs
+++ b/libraries/ghc-prim/GHC/Magic/Dict.hs
@@ -29,7 +29,9 @@
 --
 -----------------------------------------------------------------------------
 
-module GHC.Magic.Dict (WithDict(..)) where
+module GHC.Magic.Dict (
+    WithDict( withDict )
+  ) where
 
 import GHC.Types (RuntimeRep, TYPE)
 
@@ -57,4 +59,4 @@ there is nothing that forces the `cls` Wanted from the call to `k` to unify with
 
 That's fine.  But it means we need -XAllowAmbiguousTypes for the withDict definition,
 at least with deep subsumption.
--}
\ No newline at end of file
+-}
diff --git a/libraries/ghc-prim/GHC/Prim/Panic.hs b/libraries/ghc-prim/GHC/Prim/Panic.hs
index a6f1eb588b..a24f82ee07 100644
--- a/libraries/ghc-prim/GHC/Prim/Panic.hs
+++ b/libraries/ghc-prim/GHC/Prim/Panic.hs
@@ -4,6 +4,7 @@
 {-# LANGUAGE UnboxedTuples #-}
 {-# LANGUAGE NoImplicitPrelude #-}
 {-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE RankNTypes, KindSignatures #-}
 
 -- | Primitive panics.
 --
@@ -11,12 +12,13 @@
 module GHC.Prim.Panic
    ( absentSumFieldError
    , panicError
-   , absentError
+   , absentError, absentConstraintError
    )
 where
 
 import GHC.Prim
 import GHC.Magic
+import GHC.Types( Type )
 
 default () -- Double and Integer aren't available yet
 
@@ -95,7 +97,7 @@ absentSumFieldError = panicError "entered absent sum field!"#
 
 -- | Displays "Oops!  Entered absent arg" ++ errormsg and exits the program.
 {-# NOINLINE absentError #-}
-absentError :: Addr# -> a
+absentError :: forall (a :: Type). Addr# -> a
 absentError errmsg =
   runRW# (\s ->
     case stg_absentError# errmsg s of
@@ -103,3 +105,15 @@ absentError errmsg =
                     -- use an empty case lest the pattern match
                     -- checker squawks.
                     let x = x in x)
+
+{-# NOINLINE absentConstraintError #-}
+absentConstraintError :: forall (a :: Type). Addr# -> a
+-- We want to give this the type
+--    forall (a :: Constraint). Addr# -> a
+-- but Haskell source code doesn't allow functions that return Constraint
+-- Fortunately, absentConstraintError is a wired-in Id with the above
+-- desired type. So the only purpose of this definition is to give a
+-- function to call. And for that purpose, absentError will do fine.
+-- It's fine to lie about about the type; it is not looked at
+-- because absentConstraintError is wired-in.
+absentConstraintError errmsg = absentError errmsg
diff --git a/libraries/ghc-prim/GHC/Types.hs b/libraries/ghc-prim/GHC/Types.hs
index 9fdc1ac366..1ea6bd9baa 100644
--- a/libraries/ghc-prim/GHC/Types.hs
+++ b/libraries/ghc-prim/GHC/Types.hs
@@ -1,7 +1,7 @@
 {-# LANGUAGE MagicHash, NoImplicitPrelude, TypeFamilies, UnboxedTuples,
              MultiParamTypeClasses, RoleAnnotations, CPP, TypeOperators,
              PolyKinds, NegativeLiterals, DataKinds, ScopedTypeVariables,
-             TypeApplications, StandaloneKindSignatures,
+             TypeApplications, StandaloneKindSignatures, GADTs,
              FlexibleInstances, UndecidableInstances #-}
 -- NegativeLiterals: see Note [Fixity of (->)]
 {-# OPTIONS_HADDOCK print-explicit-runtime-reps #-}
@@ -40,7 +40,8 @@ module GHC.Types (
         type (~), type (~~), Coercible,
 
         -- * Representation polymorphism
-        TYPE, Levity(..), RuntimeRep(..),
+        TYPE, CONSTRAINT,
+        Levity(..), RuntimeRep(..),
         LiftedRep, UnliftedRep,
         Type, UnliftedType, Constraint,
           -- The historical type * should ideally be written as
@@ -50,6 +51,11 @@ module GHC.Types (
         VecCount(..), VecElem(..),
         Void#,
 
+        -- * Boxing constructors
+        DictBox( MkDictBox ),
+        WordBox( MkWordBox), IntBox( MkIntBox),
+        FloatBox( MkFloatBox), DoubleBox( MkDoubleBox),
+
         -- * Multiplicity types
         Multiplicity(..), MultMul,
 
@@ -62,7 +68,6 @@ import GHC.Prim
 
 infixr 5 :
 
-
 {- *********************************************************************
 *                                                                      *
                   Functions
@@ -92,8 +97,7 @@ type (->) = FUN 'Many
 *                                                                      *
 ********************************************************************* -}
 
--- | The kind of constraints, like @Show a@
-data Constraint
+
 
 -- | The runtime representation of lifted types.
 type LiftedRep = 'BoxedRep 'Lifted
@@ -106,6 +110,9 @@ type UnliftedRep = 'BoxedRep 'Unlifted
 type ZeroBitRep = 'TupleRep '[]
 
 -------------------------
+-- | The kind of lifted constraints
+type Constraint = CONSTRAINT LiftedRep
+
 -- | The kind of types with lifted values. For example @Int :: Type@.
 type Type = TYPE LiftedRep
 
@@ -473,7 +480,7 @@ data RuntimeRep = VecRep VecCount VecElem   -- ^ a SIMD vector type
 -- RuntimeRep is intimately tied to TyCon.RuntimeRep (in GHC proper). See
 -- Note [RuntimeRep and PrimRep] in RepType.
 -- See also Note [Wiring in RuntimeRep] in GHC.Builtin.Types
--- See also Note [TYPE and RuntimeRep] in GHC.Builtin.Type.Prim
+-- See also Note [TYPE and CONSTRAINT] in GHC.Builtin.Type.Prim
 
 -- | Length of a SIMD vector type
 data VecCount = Vec2
@@ -502,6 +509,37 @@ type Void# = (# #)
 
 {- *********************************************************************
 *                                                                      *
+             Boxing data constructors
+*                                                                      *
+********************************************************************* -}
+
+-- These "boxing" data types allow us to wrap up a value of kind (TYPE rr)
+-- in a box of kind Type, for each rr.
+data LiftBox   (a :: TYPE UnliftedRep) = MkLiftBox a
+
+data IntBox    (a :: TYPE IntRep)      = MkIntBox a
+data Int8Box   (a :: TYPE Int8Rep)     = MkInt8Box a
+data Int16Box  (a :: TYPE Int16Rep)    = MkInt16Box a
+data Int32Box  (a :: TYPE Int32Rep)    = MkInt32Box a
+data Int64Box  (a :: TYPE Int64Rep)    = MkInt64Box a
+
+data WordBox   (a :: TYPE WordRep)     = MkWordBox a
+data Word8Box  (a :: TYPE Word8Rep)    = MkWord8Box a
+data Word16Box (a :: TYPE Word16Rep)   = MkWord16Box a
+data Word32Box (a :: TYPE Word32Rep)   = MkWord32Box a
+data Word64Box (a :: TYPE Word64Rep)   = MkWord64Box a
+
+data FloatBox  (a :: TYPE FloatRep)    = MkFloatBox a
+data DoubleBox (a :: TYPE DoubleRep)   = MkDoubleBox a
+
+-- | Data type `Dict` provides a simple way to wrap up a (lifted)
+--   constraint as a type
+data DictBox c where
+  MkDictBox :: c => DictBox c
+
+
+{- *********************************************************************
+*                                                                      *
              Runtime representation of TyCon
 *                                                                      *
 ********************************************************************* -}