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

3 files changed, 105 insertions, 71 deletions

diff --git a/compiler/GHC/Tc/Instance/Class.hs b/compiler/GHC/Tc/Instance/Class.hs
index 0d96d4420e..57ee52144c 100644
--- a/compiler/GHC/Tc/Instance/Class.hs
+++ b/compiler/GHC/Tc/Instance/Class.hs
@@ -38,6 +38,7 @@ import GHC.Types.Id.Make ( nospecId )
 import GHC.Types.Var
 
 import GHC.Core.Predicate
+import GHC.Core.Coercion
 import GHC.Core.InstEnv
 import GHC.Core.Type
 import GHC.Core.Make ( mkCharExpr, mkNaturalExpr, mkStringExprFS, mkCoreLams )
@@ -54,8 +55,6 @@ import GHC.Data.FastString
 
 import Language.Haskell.Syntax.Basic (FieldLabelString(..))
 
-import Data.Maybe
-
 {- *******************************************************************
 *                                                                    *
               A helper for associated types within
@@ -154,20 +153,17 @@ matchGlobalInst :: DynFlags
                              -- See Note [Shortcut solving: overlap]
                 -> Class -> [Type] -> TcM ClsInstResult
 matchGlobalInst dflags short_cut clas tys
-  | cls_name == knownNatClassName
-  = matchKnownNat    dflags short_cut clas tys
-  | cls_name == knownSymbolClassName
-  = matchKnownSymbol dflags short_cut clas tys
-  | cls_name == knownCharClassName
-  = matchKnownChar dflags short_cut clas tys
-  | isCTupleClass clas                = matchCTuple          clas tys
-  | cls_name == typeableClassName     = matchTypeable        clas tys
-  | cls_name == withDictClassName     = matchWithDict             tys
-  | clas `hasKey` heqTyConKey         = matchHeteroEquality       tys
-  | clas `hasKey` eqTyConKey          = matchHomoEquality         tys
-  | clas `hasKey` coercibleTyConKey   = matchCoercible            tys
-  | cls_name == hasFieldClassName     = matchHasField dflags short_cut clas tys
-  | otherwise                         = matchInstEnv dflags short_cut clas tys
+  | cls_name == knownNatClassName     = matchKnownNat    dflags short_cut clas tys
+  | cls_name == knownSymbolClassName  = matchKnownSymbol dflags short_cut clas tys
+  | cls_name == knownCharClassName    = matchKnownChar   dflags short_cut clas tys
+  | isCTupleClass clas                = matchCTuple                       clas tys
+  | cls_name == typeableClassName     = matchTypeable                     clas tys
+  | cls_name == withDictClassName     = matchWithDict                          tys
+  | clas `hasKey` heqTyConKey         = matchHeteroEquality                    tys
+  | clas `hasKey` eqTyConKey          = matchHomoEquality                      tys
+  | clas `hasKey` coercibleTyConKey   = matchCoercible                         tys
+  | cls_name == hasFieldClassName     = matchHasField    dflags short_cut clas tys
+  | otherwise                         = matchInstEnv     dflags short_cut clas tys
   where
     cls_name = className clas
 
@@ -193,7 +189,7 @@ matchInstEnv dflags short_cut_solver clas tys
 
             -- Nothing matches
             ([], NoUnifiers, _)
-                -> do { traceTc "matchClass not matching" (ppr pred)
+                -> do { traceTc "matchClass not matching" (ppr pred $$ ppr (ie_local instEnvs))
                       ; return NoInstance }
 
             -- A single match (& no safe haskell failure)
@@ -427,7 +423,7 @@ makeLitDict clas ty et
                     -- then tcRep is SNat
     , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty]
           -- SNat n ~ Integer
-    , let ev_tm = mkEvCast et (mkTcSymCo (mkTcTransCo co_dict co_rep))
+    , let ev_tm = mkEvCast et (mkSymCo (mkTransCo co_dict co_rep))
     = return $ OneInst { cir_new_theta = []
                        , cir_mk_ev     = \_ -> ev_tm
                        , cir_what      = BuiltinInstance }
@@ -454,8 +450,8 @@ matchWithDict [cls, mty]
     -- and in that case let
     -- co :: C t1 ..tn ~R# inst_meth_ty
   , Just (inst_meth_ty, co) <- tcInstNewTyCon_maybe dict_tc dict_args
-  = do { sv <- mkSysLocalM (fsLit "withDict_s") Many mty
-       ; k  <- mkSysLocalM (fsLit "withDict_k") Many (mkInvisFunTyMany cls openAlphaTy)
+  = do { sv <- mkSysLocalM (fsLit "withDict_s") ManyTy mty
+       ; k  <- mkSysLocalM (fsLit "withDict_k") ManyTy (mkInvisFunTy cls openAlphaTy)
 
        -- Given co2 : mty ~N# inst_meth_ty, construct the method of
        -- the WithDict dictionary:
@@ -472,11 +468,11 @@ matchWithDict [cls, mty]
                mkCoreLams [ runtimeRep1TyVar, openAlphaTyVar, sv, k ] $
                  Var nospecId
                    `App`
-                 (Type $ mkInvisFunTyMany cls openAlphaTy)
+                 (Type $ mkInvisFunTy cls openAlphaTy)
                    `App`
                  Var k
                    `App`
-                 (Var sv `Cast` mkTcTransCo (mkTcSubCo co2) (mkTcSymCo co))
+                 (Var sv `Cast` mkTransCo (mkSubCo co2) (mkSymCo co))
 
        ; tc <- tcLookupTyCon withDictClassName
        ; let Just withdict_data_con
@@ -646,18 +642,29 @@ Some further observations about `withDict`:
 -- and it was applied to the correct argument.
 matchTypeable :: Class -> [Type] -> TcM ClsInstResult
 matchTypeable clas [k,t]  -- clas = Typeable
-  -- For the first two cases, See Note [No Typeable for polytypes or qualified types]
-  | isForAllTy k                      = return NoInstance   -- Polytype
-  | isJust (tcSplitPredFunTy_maybe t) = return NoInstance   -- Qualified type
+  -- Forall types: see Note [No Typeable for polytypes or qualified types]
+  | isForAllTy k = return NoInstance
+
+  -- Functions; but only with a visible argment
+  | Just (af,mult,arg,ret) <- splitFunTy_maybe t
+  = if isVisibleFunArg af
+    then doFunTy clas t mult arg ret
+    else return NoInstance
+      -- 'else' case: qualified types like (Num a => blah) are not typeable
+      -- see Note [No Typeable for polytypes or qualified types]
 
   -- Now cases that do work
-  | k `eqType` naturalTy                   = doTyLit knownNatClassName         t
-  | k `eqType` typeSymbolKind              = doTyLit knownSymbolClassName      t
-  | k `eqType` charTy                      = doTyLit knownCharClassName        t
-  | tcIsConstraintKind t                   = doTyConApp clas t constraintKindTyCon []
-  | Just (mult,arg,ret) <- splitFunTy_maybe t   = doFunTy    clas t mult arg ret
+  | k `eqType` naturalTy      = doTyLit knownNatClassName         t
+  | k `eqType` typeSymbolKind = doTyLit knownSymbolClassName      t
+  | k `eqType` charTy         = doTyLit knownCharClassName        t
+
+  -- TyCon applied to its kind args
+  -- No special treatment of Type and Constraint; they get distinct TypeReps
+  -- see wrinkle (W4) of Note [Type and Constraint are not apart]
+  --     in GHC.Builtin.Types.Prim.
   | Just (tc, ks) <- splitTyConApp_maybe t -- See Note [Typeable (T a b c)]
   , onlyNamedBndrsApplied tc ks            = doTyConApp clas t tc ks
+
   | Just (f,kt)   <- splitAppTy_maybe t    = doTyApp    clas t f kt
 
 matchTypeable _ _ = return NoInstance
@@ -681,10 +688,9 @@ doFunTy clas ty mult arg_ty ret_ty
 doTyConApp :: Class -> Type -> TyCon -> [Kind] -> TcM ClsInstResult
 doTyConApp clas ty tc kind_args
   | tyConIsTypeable tc
-  = do
-     return $ OneInst { cir_new_theta = (map (mk_typeable_pred clas) kind_args)
-                      , cir_mk_ev     = mk_ev
-                      , cir_what      = BuiltinTypeableInstance tc }
+  = return $ OneInst { cir_new_theta = map (mk_typeable_pred clas) kind_args
+                     , cir_mk_ev     = mk_ev
+                     , cir_what      = BuiltinTypeableInstance tc }
   | otherwise
   = return NoInstance
   where
@@ -710,7 +716,7 @@ doTyApp :: Class -> Type -> Type -> KindOrType -> TcM ClsInstResult
 --    (Typeable f, Typeable Int, Typeable Char)  --> (after some simp. steps)
 --    Typeable f
 doTyApp clas ty f tk
-  | isForAllTy (tcTypeKind f)
+  | isForAllTy (typeKind f)
   = return NoInstance -- We can't solve until we know the ctr.
   | otherwise
   = return $ OneInst { cir_new_theta = map (mk_typeable_pred clas) [f, tk]
@@ -723,7 +729,7 @@ doTyApp clas ty f tk
 
 -- Emit a `Typeable` constraint for the given type.
 mk_typeable_pred :: Class -> Type -> PredType
-mk_typeable_pred clas ty = mkClassPred clas [ tcTypeKind ty, ty ]
+mk_typeable_pred clas ty = mkClassPred clas [ typeKind ty, ty ]
 
   -- Typeable is implied by KnownNat/KnownSymbol. In the case of a type literal
   -- we generate a sub-goal for the appropriate class.
@@ -739,14 +745,31 @@ doTyLit kc t = do { kc_clas <- tcLookupClass kc
 
 {- Note [Typeable (T a b c)]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
 For type applications we always decompose using binary application,
-via doTyApp, until we get to a *kind* instantiation.  Example
-   Proxy :: forall k. k -> *
+via doTyApp (building a TrApp), until we get to a *kind* instantiation
+(building a TrTyCon).  We detect a pure kind instantiation using
+`onlyNamedBndrsApplied`.
+
+Example: Proxy :: forall k. k -> *
+
+  To solve Typeable (Proxy @(* -> *) Maybe) we
+
+  - First decompose with doTyApp (onlyNamedBndrsApplied is False)
+    to get (Typeable (Proxy @(* -> *))) and Typeable Maybe.
+    This step returns a TrApp.
+
+  - Then solve (Typeable (Proxy @(* -> *))) with doTyConApp
+    (onlyNamedBndrsApplied is True).
+    This step returns a TrTyCon
+
+  So the TypeRep we build is
+    TrApp (TrTyCon ("Proxy" @(*->*))) (TrTyCon "Maybe")
 
-To solve Typeable (Proxy (* -> *) Maybe) we
-  - First decompose with doTyApp,
-    to get (Typeable (Proxy (* -> *))) and Typeable Maybe
-  - Then solve (Typeable (Proxy (* -> *))) with doTyConApp
+Notice also that TYPE and CONSTRAINT are distinct so, in effect, we
+allow (Typeable TYPE) and (Typeable CONSTRAINT), giving disinct TypeReps.
+This is very important: we may want to get a TypeRep for a kind like
+   Type -> Constraint
 
 If we attempt to short-cut by solving it all at once, via
 doTyConApp
@@ -939,8 +962,8 @@ matchHasField dflags short_cut clas tys
                          -- it to a HasField dictionary.
                          mk_ev (ev1:evs) = evSelector sel_id tvs evs `evCast` co
                            where
-                             co = mkTcSubCo (evTermCoercion (EvExpr ev1))
-                                      `mkTcTransCo` mkTcSymCo co2
+                             co = mkSubCo (evTermCoercion (EvExpr ev1))
+                                      `mkTransCo` mkSymCo co2
                          mk_ev [] = panic "matchHasField.mk_ev"
 
                          Just (_, co2) = tcInstNewTyCon_maybe (classTyCon clas)
diff --git a/compiler/GHC/Tc/Instance/FunDeps.hs b/compiler/GHC/Tc/Instance/FunDeps.hs
index 710750a57d..681fd5d9a2 100644
--- a/compiler/GHC/Tc/Instance/FunDeps.hs
+++ b/compiler/GHC/Tc/Instance/FunDeps.hs
@@ -29,14 +29,18 @@ import GHC.Types.Var
 import GHC.Core.Class
 import GHC.Core.Predicate
 import GHC.Core.Type
-import GHC.Tc.Utils.TcType( transSuperClasses )
+import GHC.Core.RoughMap( RoughMatchTc(..) )
 import GHC.Core.Coercion.Axiom( TypeEqn )
 import GHC.Core.Unify
 import GHC.Core.InstEnv
-import GHC.Types.Var.Set
-import GHC.Types.Var.Env
 import GHC.Core.TyCo.FVs
+import GHC.Core.TyCo.Compare( eqTypes, eqType )
 import GHC.Core.TyCo.Ppr( pprWithExplicitKindsWhen )
+
+import GHC.Tc.Utils.TcType( transSuperClasses )
+
+import GHC.Types.Var.Set
+import GHC.Types.Var.Env
 import GHC.Types.SrcLoc
 
 import GHC.Utils.Outputable
@@ -122,11 +126,12 @@ Wrinkles:
        [W] D Int Bool ty
 
     Then we'll generate
-       FDEqn { fd_qtvs = [x], fd_eqs = [Pair x Bool, Pair (Maybe x) ty] }
+       FDEqn { fd_qtvs = [x0], fd_eqs = [ x0 ~ Bool, Maybe x0 ~ ty] }
+    which generates one fresh unification variable x0
 
     But if the fundeps had been (a->b, a->c) we'd generate two FDEqns
-       FDEqn { fd_qtvs = [x], fd_eqs = [Pair x Bool] }
-       FDEqn { fd_qtvs = [x], fd_eqs = [Pair (Maybe x) ty] }
+       FDEqn { fd_qtvs = [x1], fd_eqs = [ x1 ~ Bool ] }
+       FDEqn { fd_qtvs = [x2], fd_eqs = [ Maybe x2 ~ ty ] }
     with two FDEqns, generating two separate unification variables.
 
 (3) improveFromInstEnv doesn't return any equations that already hold.
@@ -405,7 +410,7 @@ checkInstCoverage be_liberal clas theta inst_taus
        where
          (ls,rs) = instFD fd tyvars inst_taus
          ls_tvs = tyCoVarsOfTypes ls
-         rs_tvs = splitVisVarsOfTypes rs
+         rs_tvs = visVarsOfTypes rs
 
          undetermined_tvs | be_liberal = liberal_undet_tvs
                           | otherwise  = conserv_undet_tvs
diff --git a/compiler/GHC/Tc/Instance/Typeable.hs b/compiler/GHC/Tc/Instance/Typeable.hs
index d5ad9b5186..9de6aa9e94 100644
--- a/compiler/GHC/Tc/Instance/Typeable.hs
+++ b/compiler/GHC/Tc/Instance/Typeable.hs
@@ -13,7 +13,7 @@ module GHC.Tc.Instance.Typeable(mkTypeableBinds, tyConIsTypeable) where
 import GHC.Prelude
 import GHC.Platform
 
-import GHC.Types.Basic ( Boxity(..), neverInlinePragma )
+import GHC.Types.Basic ( Boxity(..), TypeOrConstraint(..), neverInlinePragma )
 import GHC.Types.SourceText ( SourceText(..) )
 import GHC.Iface.Env( newGlobalBinder )
 import GHC.Core.TyCo.Rep( Type(..), TyLit(..) )
@@ -330,9 +330,11 @@ mkPrimTypeableTodos
 
                      -- Build TypeRepTodos for built-in KindReps
                    ; todo1 <- todoForExportedKindReps builtInKindReps
+
                      -- Build TypeRepTodos for types in GHC.Prim
                    ; todo2 <- todoForTyCons gHC_PRIM ghc_prim_module_id
                                             ghcPrimTypeableTyCons
+
                    ; return ( gbl_env' , [todo1, todo2])
                    }
            else do gbl_env <- getGblEnv
@@ -406,7 +408,7 @@ mkTyConRepBinds :: TypeableStuff -> TypeRepTodo
                 -> TypeableTyCon -> KindRepM (LHsBinds GhcTc)
 mkTyConRepBinds stuff todo (TypeableTyCon {..})
   = do -- Make a KindRep
-       let (bndrs, kind) = splitForAllTyCoVarBinders (tyConKind tycon)
+       let (bndrs, kind) = splitForAllForAllTyBinders (tyConKind tycon)
        liftTc $ traceTc "mkTyConKindRepBinds"
                         (ppr tycon $$ ppr (tyConKind tycon) $$ ppr kind)
        let ctx = mkDeBruijnContext (map binderVar bndrs)
@@ -420,9 +422,8 @@ mkTyConRepBinds stuff todo (TypeableTyCon {..})
 -- | Is a particular 'TyCon' representable by @Typeable@?. These exclude type
 -- families and polytypes.
 tyConIsTypeable :: TyCon -> Bool
-tyConIsTypeable tc =
-       isJust (tyConRepName_maybe tc)
-    && kindIsTypeable (dropForAlls $ tyConKind tc)
+tyConIsTypeable tc = isJust (tyConRepName_maybe tc)
+                  && kindIsTypeable (dropForAlls $ tyConKind tc)
 
 -- | Is a particular 'Kind' representable by @Typeable@? Here we look for
 -- polytypes and types containing casts (which may be, for instance, a type
@@ -464,12 +465,14 @@ newtype KindRepM a = KindRepM { unKindRepM :: StateT KindRepEnv TcRn a }
 liftTc :: TcRn a -> KindRepM a
 liftTc = KindRepM . lift
 
--- | We generate @KindRep@s for a few common kinds in @GHC.Types@ so that they
+-- | We generate `KindRep`s for a few common kinds, so that they
 -- can be reused across modules.
+-- These definitions are generated in `ghc-prim:GHC.Types`.
 builtInKindReps :: [(Kind, Name)]
 builtInKindReps =
-    [ (star, starKindRepName)
-    , (mkVisFunTyMany star star, starArrStarKindRepName)
+    [ (star,                              starKindRepName)
+    , (constraintKind,                    constraintKindRepName)
+    , (mkVisFunTyMany star star,          starArrStarKindRepName)
     , (mkVisFunTysMany [star, star] star, starArrStarArrStarKindRepName)
     ]
   where
@@ -481,6 +484,7 @@ initialKindRepEnv = foldlM add_kind_rep emptyTypeMap builtInKindReps
     add_kind_rep acc (k,n) = do
         id <- tcLookupId n
         return $! extendTypeMap acc k (id, Nothing)
+        -- The TypeMap looks through type synonyms
 
 -- | Performed while compiling "GHC.Types" to generate the built-in 'KindRep's.
 mkExportedKindReps :: TypeableStuff
@@ -496,6 +500,7 @@ mkExportedKindReps stuff = mapM_ kindrep_binding
         -- since the latter would find the built-in 'KindRep's in the
         -- 'KindRepEnv' (by virtue of being in 'initialKindRepEnv').
         rhs <- mkKindRepRhs stuff empty_scope kind
+        liftTc (traceTc "mkExport" (ppr kind $$ ppr rep_bndr $$ ppr rhs))
         addKindRepBind empty_scope kind rep_bndr rhs
 
 addKindRepBind :: CmEnv -> Kind -> Id -> LHsExpr GhcTc -> KindRepM ()
@@ -528,10 +533,8 @@ getKindRep stuff@(Stuff {..}) in_scope = go
 
     go' :: Kind -> KindRepEnv -> TcRn (LHsExpr GhcTc, KindRepEnv)
     go' k env
-        -- Look through type synonyms
-      | Just k' <- tcView k = go' k' env
-
         -- We've already generated the needed KindRep
+        -- This lookup looks through synonyms
       | Just (id, _) <- lookupTypeMapWithScope env in_scope k
       = return (nlHsVar id, env)
 
@@ -540,7 +543,7 @@ getKindRep stuff@(Stuff {..}) in_scope = go
       = do -- Place a NOINLINE pragma on KindReps since they tend to be quite
            -- large and bloat interface files.
            rep_bndr <- (`setInlinePragma` neverInlinePragma)
-                   <$> newSysLocalId (fsLit "$krep") Many (mkTyConTy kindRepTyCon)
+                   <$> newSysLocalId (fsLit "$krep") ManyTy (mkTyConTy kindRepTyCon)
 
            -- do we need to tie a knot here?
            flip runStateT env $ unKindRepM $ do
@@ -560,24 +563,27 @@ mkKindRepRhs stuff@(Stuff {..}) in_scope = new_kind_rep_shortcut
         -- We handle (TYPE LiftedRep) etc separately to make it
         -- clear to consumers (e.g. serializers) that there is
         -- a loop here (as TYPE :: RuntimeRep -> TYPE 'LiftedRep)
-      | not (tcIsConstraintKind k)
+      | Just (TypeLike, rep) <- sORTKind_maybe k
               -- Typeable respects the Constraint/Type distinction
               -- so do not follow the special case here
-      , Just arg <- kindRep_maybe k
-      = case splitTyConApp_maybe arg of
-          Just (tc, [])
+      = -- Here k = TYPE <something>
+        case splitTyConApp_maybe rep of
+          Just (tc, [])         -- TYPE IntRep, TYPE FloatRep etc
             | Just dc <- isPromotedDataCon_maybe tc
               -> return $ nlHsDataCon kindRepTYPEDataCon `nlHsApp` nlHsDataCon dc
 
-          Just (rep, [levArg])
-            | Just dcRep <- isPromotedDataCon_maybe rep
-            , Just (lev, []) <- splitTyConApp_maybe levArg
-            , Just dcLev <- isPromotedDataCon_maybe lev
+          Just (rep_tc, [levArg])  -- TYPE (BoxedRep lev)
+            | Just dcRep <- isPromotedDataCon_maybe rep_tc
+            , Just (lev_tc, []) <- splitTyConApp_maybe levArg
+            , Just dcLev <- isPromotedDataCon_maybe lev_tc
               -> return $ nlHsDataCon kindRepTYPEDataCon `nlHsApp` (nlHsDataCon dcRep `nlHsApp` nlHsDataCon dcLev)
 
           _   -> new_kind_rep k
       | otherwise = new_kind_rep k
 
+    new_kind_rep ki  -- Expand synonyms
+      | Just ki' <- coreView ki
+      = new_kind_rep ki'
 
     new_kind_rep (TyVarTy v)
       | Just idx <- lookupCME in_scope v