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

1 files changed, 26 insertions, 24 deletions

diff --git a/compiler/GHC/Tc/Gen/App.hs b/compiler/GHC/Tc/Gen/App.hs
index b420cf8c9e..c44fb65a29 100644
--- a/compiler/GHC/Tc/Gen/App.hs
+++ b/compiler/GHC/Tc/Gen/App.hs
@@ -40,6 +40,7 @@ import GHC.Core.TyCo.Ppr
 import GHC.Core.TyCo.Subst (substTyWithInScope)
 import GHC.Core.TyCo.FVs( shallowTyCoVarsOfType )
 import GHC.Core.Type
+import GHC.Core.Coercion
 import GHC.Tc.Types.Evidence
 import GHC.Types.Var.Set
 import GHC.Builtin.PrimOps( tagToEnumKey )
@@ -544,7 +545,7 @@ tcInstFun do_ql inst_final (rn_fun, fun_ctxt) fun_sigma rn_args
           HsUnboundVar {} -> True
           _               -> False
 
-    inst_all, inst_inferred, inst_none :: ArgFlag -> Bool
+    inst_all, inst_inferred, inst_none :: ForAllTyFlag -> Bool
     inst_all (Invisible {}) = True
     inst_all Required       = False
 
@@ -554,7 +555,7 @@ tcInstFun do_ql inst_final (rn_fun, fun_ctxt) fun_sigma rn_args
 
     inst_none _ = False
 
-    inst_fun :: [HsExprArg 'TcpRn] -> ArgFlag -> Bool
+    inst_fun :: [HsExprArg 'TcpRn] -> ForAllTyFlag -> Bool
     inst_fun [] | inst_final  = inst_all
                 | otherwise   = inst_none
                 -- Using `inst_none` for `:type` avoids
@@ -573,7 +574,7 @@ tcInstFun do_ql inst_final (rn_fun, fun_ctxt) fun_sigma rn_args
 
     -- go: If fun_ty=kappa, look it up in Theta
     go delta acc so_far fun_ty args
-      | Just kappa <- tcGetTyVar_maybe fun_ty
+      | Just kappa <- getTyVar_maybe fun_ty
       , kappa `elemVarSet` delta
       = do { cts <- readMetaTyVar kappa
            ; case cts of
@@ -624,7 +625,7 @@ tcInstFun do_ql inst_final (rn_fun, fun_ctxt) fun_sigma rn_args
 
     -- Rule IVAR from Fig 4 of the QL paper:
     go1 delta acc so_far fun_ty args@(EValArg {} : _)
-      | Just kappa <- tcGetTyVar_maybe fun_ty
+      | Just kappa <- getTyVar_maybe fun_ty
       , kappa `elemVarSet` delta
       = -- Function type was of form   f :: forall a b. t1 -> t2 -> b
         -- with 'b', one of the quantified type variables, in the corner
@@ -651,8 +652,8 @@ tcInstFun do_ql inst_final (rn_fun, fun_ctxt) fun_sigma rn_args
            ; let delta'  = delta `extendVarSetList` (res_nu:arg_nus)
                  arg_tys = mkTyVarTys arg_nus
                  res_ty  = mkTyVarTy res_nu
-                 fun_ty' = mkVisFunTys (zipWithEqual "tcInstFun" mkScaled mults arg_tys) res_ty
-                 co_wrap = mkWpCastN (mkTcGReflLeftCo Nominal fun_ty' kind_co)
+                 fun_ty' = mkScaledFunTys (zipWithEqual "tcInstFun" mkScaled mults arg_tys) res_ty
+                 co_wrap = mkWpCastN (mkGReflLeftCo Nominal fun_ty' kind_co)
                  acc'    = addArgWrap co_wrap acc
                  -- Suppose kappa :: kk
                  -- Then fun_ty :: kk, fun_ty' :: Type, kind_co :: Type ~ kk
@@ -716,7 +717,7 @@ tcVTA :: TcType            -- Function type
 -- The function type has already had its Inferred binders instantiated
 tcVTA fun_ty hs_ty
   | Just (tvb, inner_ty) <- tcSplitForAllTyVarBinder_maybe fun_ty
-  , binderArgFlag tvb == Specified
+  , binderFlag tvb == Specified
     -- It really can't be Inferred, because we've just
     -- instantiated those. But, oddly, it might just be Required.
     -- See Note [Required quantifiers in the type of a term]
@@ -731,11 +732,12 @@ tcVTA fun_ty hs_ty
              insted_ty = substTyWithInScope in_scope [tv] [ty_arg] inner_ty
                          -- NB: tv and ty_arg have the same kind, so this
                          --     substitution is kind-respecting
-       ; traceTc "VTA" (vcat [ppr tv, debugPprType kind
-                             , debugPprType ty_arg
-                             , debugPprType (tcTypeKind ty_arg)
-                             , debugPprType inner_ty
-                             , debugPprType insted_ty ])
+       ; traceTc "VTA" (vcat [ text "fun_ty" <+> ppr fun_ty
+                             , text "tv" <+> ppr tv <+> dcolon <+> debugPprType kind
+                             , text "ty_arg" <+> debugPprType ty_arg <+> dcolon
+                                             <+> debugPprType (typeKind ty_arg)
+                             , text "inner_ty" <+> debugPprType inner_ty
+                             , text "insted_ty" <+> debugPprType insted_ty ])
        ; return (ty_arg, insted_ty) }
 
   | otherwise
@@ -758,7 +760,7 @@ whose first argument is Required
 We want to reject this type application to Int, but in earlier
 GHCs we had an ASSERT that Required could not occur here.
 
-The ice is thin; c.f. Note [No Required TyCoBinder in terms]
+The ice is thin; c.f. Note [No Required PiTyBinder in terms]
 in GHC.Core.TyCo.Rep.
 
 Note [VTA for out-of-scope functions]
@@ -876,7 +878,7 @@ quickLookArg delta larg (Scaled _ arg_ty)
               -- This top-level zonk step, which is the reason
               -- we need a local 'go' loop, is subtle
               -- See Section 9 of the QL paper
-              | Just kappa <- tcGetTyVar_maybe arg_ty
+              | Just kappa <- getTyVar_maybe arg_ty
               , kappa `elemVarSet` delta
               = do { info <- readMetaTyVar kappa
                    ; case info of
@@ -990,8 +992,8 @@ qlUnify delta ty1 ty2
 
     -- Now, and only now, expand synonyms
     go bvs rho1 rho2
-      | Just rho1 <- tcView rho1 = go bvs rho1 rho2
-      | Just rho2 <- tcView rho2 = go bvs rho1 rho2
+      | Just rho1 <- coreView rho1 = go bvs rho1 rho2
+      | Just rho2 <- coreView rho2 = go bvs rho1 rho2
 
     go bvs (TyConApp tc1 tys1) (TyConApp tc2 tys2)
       | tc1 == tc2
@@ -1001,25 +1003,25 @@ qlUnify delta ty1 ty2
 
     -- Decompose (arg1 -> res1) ~ (arg2 -> res2)
     -- and         (c1 => res1) ~   (c2 => res2)
-    -- But for the latter we only learn instantiation info from t1~t2
+    -- But for the latter we only learn instantiation info from res1~res2
     -- We look at the multiplicity too, although the chances of getting
     -- impredicative instantiation info from there seems...remote.
     go bvs (FunTy { ft_af = af1, ft_arg = arg1, ft_res = res1, ft_mult = mult1 })
            (FunTy { ft_af = af2, ft_arg = arg2, ft_res = res2, ft_mult = mult2 })
-      | af1 == af2
-      = do { when (af1 == VisArg) $
-             do { go bvs arg1 arg2; go bvs mult1 mult2 }
+      | af1 == af2 -- Match the arrow TyCon
+      = do { when (isVisibleFunArg af1) (go bvs arg1 arg2)
+           ; when (isFUNArg af1)        (go bvs mult1 mult2)
            ; go bvs res1 res2 }
 
     -- ToDo: c.f. Tc.Utils.unify.uType,
     -- which does not split FunTy here
-    -- Also NB tcRepSplitAppTy here, which does not split (c => t)
+    -- Also NB tcSplitAppTyNoView here, which does not split (c => t)
     go bvs (AppTy t1a t1b) ty2
-      | Just (t2a, t2b) <- tcRepSplitAppTy_maybe ty2
+      | Just (t2a, t2b) <- tcSplitAppTyNoView_maybe ty2
       = do { go bvs t1a t2a; go bvs t1b t2b }
 
     go bvs ty1 (AppTy t2a t2b)
-      | Just (t1a, t1b) <- tcRepSplitAppTy_maybe ty1
+      | Just (t1a, t1b) <- tcSplitAppTyNoView_maybe ty1
       = do { go bvs t1a t2a; go bvs t1b t2b }
 
     go (bvs1, bvs2) (ForAllTy bv1 ty1) (ForAllTy bv2 ty2)
@@ -1215,7 +1217,7 @@ tcTagToEnum tc_fun fun_ctxt tc_args res_ty
          check_enumeration res_ty rep_tc
        ; let rep_ty  = mkTyConApp rep_tc rep_args
              tc_fun' = mkHsWrap (WpTyApp rep_ty) tc_fun
-             df_wrap = mkWpCastR (mkTcSymCo coi)
+             df_wrap = mkWpCastR (mkSymCo coi)
        ; tc_expr <- rebuildHsApps tc_fun' fun_ctxt [val_arg] res_ty
        ; return (mkHsWrap df_wrap tc_expr) }}}}}