Completely re-engineer the PKTI

The Purely Kinded Type Invariant (PKTI), see TcHsType,
was broken -- see #17323.

This patch fixes it beautifully, by changing mkCastTy and
mkAppTy, but getting rid of the horrid mkAppTyM.

This commit meessage should be improved, but I'm putting
the patch up for review.

8 files changed, 122 insertions, 133 deletions

diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 9a5d745dea..c9bb390f9e 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -1098,7 +1098,7 @@ tcInferApps_nosat mode orig_hs_ty fun orig_hs_args
         Named (Bndr _ Inferred) -> instantiate ki_binder inner_ki
         Anon InvisArg _         -> instantiate ki_binder inner_ki
 
-        Named (Bndr _ Specified) ->  -- Visible kind application
+        Named (Bndr tv Specified) ->  -- Visible kind application
           do { traceTc "tcInferApps (vis kind app)"
                        (vcat [ ppr ki_binder, ppr hs_ki_arg
                              , ppr (tyBinderType ki_binder)
@@ -1114,7 +1114,9 @@ tcInferApps_nosat mode orig_hs_ty fun orig_hs_args
                          tc_lhs_type (kindLevel mode) hs_ki_arg exp_kind
 
              ; traceTc "tcInferApps (vis kind app)" (ppr exp_kind)
-             ; (subst', fun') <- mkAppTyM subst fun ki_binder ki_arg
+
+             ; let subst' = extendTvSubstAndInScope subst tv ki_arg
+                   fun'   = mk_app_ty fun ki_arg
              ; go (n+1) fun' subst' inner_ki hs_args }
 
         -- Attempted visible kind application (fun @ki), but fun_ki is
@@ -1144,7 +1146,8 @@ tcInferApps_nosat mode orig_hs_ty fun orig_hs_args
                 ; arg' <- addErrCtxt (funAppCtxt orig_hs_ty arg n) $
                           tc_lhs_type mode arg exp_kind
                 ; traceTc "tcInferApps (vis normal app) 2" (ppr exp_kind)
-                ; (subst', fun') <- mkAppTyM subst fun ki_binder arg'
+                ; let subst' = extendTvSubstBinderAndInScope subst ki_binder arg'
+                      fun'   = mk_app_ty fun arg'
                 ; go (n+1) fun' subst' inner_ki args }
 
           -- no binder; try applying the substitution, or infer another arrow in fun kind
@@ -1170,9 +1173,6 @@ tcInferApps_nosat mode orig_hs_ty fun orig_hs_args
                          (vcat [ ppr ki_binder, ppr subst])
                ; (subst', arg') <- tcInstInvisibleTyBinder subst ki_binder
                ; go n (mkAppTy fun arg') subst' inner_ki all_args }
-                 -- Because tcInvisibleTyBinder instantiate ki_binder,
-                 -- the kind of arg' will have the same shape as the kind
-                 -- of ki_binder.  So we don't need mkAppTyM here.
 
         try_again_after_substing_or fallthrough
           | not (isEmptyTCvSubst subst)
@@ -1194,65 +1194,15 @@ tcInferApps_nosat mode orig_hs_ty fun orig_hs_args
       = failWith $ text "Cannot apply function of kind" <+> quotes (ppr ty)
                 $$ text "to visible kind argument" <+> quotes (ppr arg)
 
-
-mkAppTyM :: TCvSubst
-         -> TcType -> TyCoBinder    -- fun, plus its top-level binder
-         -> TcType                  -- arg
-         -> TcM (TCvSubst, TcType)  -- Extended subst, plus (fun arg)
--- Precondition: the application (fun arg) is well-kinded after zonking
---               That is, the application makes sense
---
--- Precondition: for (mkAppTyM subst fun bndr arg)
---       tcTypeKind fun  =  Pi bndr. body
---  That is, fun always has a ForAllTy or FunTy at the top
---           and 'bndr' is fun's pi-binder
---
--- Postcondition: if fun and arg satisfy (PKTI), the purely-kinded type
---                invariant, then so does the result type (fun arg)
---
--- We do not require that
---    tcTypeKind arg = tyVarKind (binderVar bndr)
--- This must be true after zonking (precondition 1), but it's not
--- required for the (PKTI).
-mkAppTyM subst fun ki_binder arg
-  | -- See Note [mkAppTyM]: Nasty case 2
-    TyConApp tc args <- fun
-  , isTypeSynonymTyCon tc
-  , args `lengthIs` (tyConArity tc - 1)
-  , any isTrickyTvBinder (tyConTyVars tc) -- We could cache this in the synonym
-  = do { arg'  <- zonkTcType  arg
-       ; args' <- zonkTcTypes args
-       ; let subst' = case ki_binder of
-                        Anon {}           -> subst
-                        Named (Bndr tv _) -> extendTvSubstAndInScope subst tv arg'
-       ; return (subst', mkTyConApp tc (args' ++ [arg'])) }
-
-
-mkAppTyM subst fun (Anon {}) arg
-   = return (subst, mk_app_ty fun arg)
-
-mkAppTyM subst fun (Named (Bndr tv _)) arg
-  = do { arg' <- if isTrickyTvBinder tv
-                 then -- See Note [mkAppTyM]: Nasty case 1
-                      zonkTcType arg
-                 else return     arg
-       ; return ( extendTvSubstAndInScope subst tv arg'
-                , mk_app_ty fun arg' ) }
-
 mk_app_ty :: TcType -> TcType -> TcType
 -- This function just adds an ASSERT for mkAppTyM's precondition
 mk_app_ty fun arg
   = ASSERT2( isPiTy fun_kind
-           ,  ppr fun <+> dcolon <+> ppr fun_kind $$ ppr arg )
+           , ppr fun <+> dcolon <+> ppr fun_kind $$ ppr arg )
     mkAppTy fun arg
   where
     fun_kind = tcTypeKind fun
 
-isTrickyTvBinder :: TcTyVar -> Bool
--- NB: isTrickyTvBinder is just an optimisation
--- It would be absolutely sound to return True always
-isTrickyTvBinder tv = isPiTy (tyVarKind tv)
-
 {- Note [The Purely Kinded Type Invariant (PKTI)]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 During type inference, we maintain this invariant
@@ -1274,48 +1224,28 @@ For example, suppose
     kappa is a unification variable
     We have already unified kappa := Type
       yielding    co :: Refl (Type -> Type)
-    a :: kappa
+    We have a type variable  a :: kappa
 then consider the type
     (a Int)
 If we call tcTypeKind on that, we'll crash, because the (un-zonked)
-kind of 'a' is just kappa, not an arrow kind.  So we must zonk first.
-
-So the type inference engine is very careful when building applications.
-This happens in tcInferApps. Suppose we are kind-checking the type (a Int),
-where (a :: kappa).  Then in tcInferApps we'll run out of binders on
-a's kind, so we'll call matchExpectedFunKind, and unify
-   kappa := kappa1 -> kappa2,  with evidence co :: kappa ~ (kappa1 ~ kappa2)
-At this point we must zonk the function type to expose the arrrow, so
-that (a Int) will satisfy (PKTI).
+kind of 'a' is just kappa, not an arrow kind.  So we instead use
+    ((a |> co) Int)
+
+For this reason, mkCastTy is very careful about discarding reflexive
+coercions.   Suppose we have
+    (mkCastTy ty co)
+and
+    ty :: k1
+    co :: k2 ~ k3
+After type inference k1=k2 always. But /during/ type inference we
+might have k1 /= k2.  Specifically,
+  * zonk(k1) = zonk(k2)
+  * k2 may be more zonked than k1, but never the other way around
+
+So mkCastTy can discard the coercion when (and only when)
+   kind( ty ) = resultKind( co )
 
 The absence of this caused #14174 and #14520.
-
-The calls to mkAppTyM is the other place we are very careful.
-
-Note [mkAppTyM]
-~~~~~~~~~~~~~~~
-mkAppTyM is trying to guarantee the Purely Kinded Type Invariant
-(PKTI) for its result type (fun arg).  There are two ways it can go wrong:
-
-* Nasty case 1: forall types (polykinds/T14174a)
-    T :: forall (p :: *->*). p Int -> p Bool
-  Now kind-check (T x), where x::kappa.
-  Well, T and x both satisfy the PKTI, but
-     T x :: x Int -> x Bool
-  and (x Int) does /not/ satisfy the PKTI.
-
-* Nasty case 2: type synonyms
-    type S f a = f a
-  Even though (S ff aa) would satisfy the (PKTI) if S was a data type
-  (i.e. nasty case 1 is dealt with), it might still not satisfy (PKTI)
-  if S is a type synonym, because the /expansion/ of (S ff aa) is
-  (ff aa), and /that/ does not satisfy (PKTI).  E.g. perhaps
-  (ff :: kappa), where 'kappa' has already been unified with (*->*).
-
-  We check for nasty case 2 on the final argument of a type synonym.
-
-Notice that in both cases the trickiness only happens if the
-bound variable has a pi-type.  Hence isTrickyTvBinder.
 -}
 
 
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 545f001f00..495305a274 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -2962,7 +2962,7 @@ rejigConRes :: [KnotTied TyConBinder] -> KnotTied Type    -- Template for result
         -- the same as the parent tycon, because checkValidDataCon will do it
 -- NB: All arguments may potentially be knot-tied
 rejigConRes tmpl_bndrs res_tmpl dc_inferred_tvs dc_specified_tvs res_ty
-        -- E.g.  data T [a] b c where
+        -- E.g.  data instance T [a] b c where
         --         MkT :: forall x y z. T [(x,y)] z z
         -- The {a,b,c} are the tmpl_tvs, and the {x,y,z} are the dc_tvs
         --     (NB: unlike the H98 case, the dc_tvs are not all existential)
@@ -2994,8 +2994,8 @@ rejigConRes tmpl_bndrs res_tmpl dc_inferred_tvs dc_specified_tvs res_ty
 
         substed_eqs = map (substEqSpec arg_subst) raw_eqs
     in
-    (univ_tvs, substed_ex_tvs, substed_inferred_tvs, substed_specified_tvs,
-     substed_eqs, arg_subst)
+    ( univ_tvs, substed_ex_tvs, substed_inferred_tvs
+    , substed_specified_tvs, substed_eqs, arg_subst)
 
   | otherwise
         -- If the return type of the data constructor doesn't match the parent
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 3f780fe546..0d10add09a 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -206,7 +206,7 @@ so we can take their type variables into account as part of the
 checkAmbiguity :: UserTypeCtxt -> Type -> TcM ()
 checkAmbiguity ctxt ty
   | wantAmbiguityCheck ctxt
-  = do { traceTc "Ambiguity check for" (ppr ty)
+  = do { traceTc "Ambiguity check for {" (ppr ty)
          -- Solve the constraints eagerly because an ambiguous type
          -- can cause a cascade of further errors.  Since the free
          -- tyvars are skolemised, we can safely use tcSimplifyTop
@@ -216,7 +216,7 @@ checkAmbiguity ctxt ty
                             tcSubType_NC ctxt ty ty
        ; simplifyAmbiguityCheck ty wanted
 
-       ; traceTc "Done ambiguity check for" (ppr ty) }
+       ; traceTc "} Done ambiguity check for" (ppr ty) }
 
   | otherwise
   = return ()
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index b338bfbf9e..cfb1b1ecd1 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -352,11 +352,19 @@ Notes:
 -}
 
 decomposePiCos :: HasDebugCallStack
-               => CoercionN -> Pair Type  -- Coercion and its kind
-               -> [Type]
+               => Kind        -- k1
+               -> CoercionN   -- co
+               -> Kind        -- k2
+               -> [Type]      -- t1 .. tn
                -> ([CoercionN], CoercionN)
+-- We have ((ty :: k1) |> (co :: kx ~ k2)) t1 .. tn
+--   and k1, k2 are the two kinds above
+-- NB: usually k1=kx, but perhaps not during type inference
+--     See Note [The Purely Kinded Type Invariant (PKTI)] in TcHsType
+--
+-- We don't pass in 'ty' at all
 -- See Note [Pushing a coercion into a pi-type]
-decomposePiCos orig_co (Pair orig_k1 orig_k2) orig_args
+decomposePiCos orig_k1 orig_co orig_k2 orig_args
   = go [] (orig_subst,orig_k1) orig_co (orig_subst,orig_k2) orig_args
   where
     orig_subst = mkEmptyTCvSubst $ mkInScopeSet $
@@ -2876,9 +2884,9 @@ simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs
       -- See Note [Last case in simplifyArgsWorker]
     go acc_xis acc_cos lc [] inner_ki roles args
       = let co1 = liftCoSubst Nominal lc inner_ki
-            co1_kind              = coercionKind co1
+            Pair flattened_kind orig_kind = coercionKind co1
             unflattened_tys       = map (coercionRKind . snd) args
-            (arg_cos, res_co)     = decomposePiCos co1 co1_kind unflattened_tys
+            (arg_cos, res_co)     = decomposePiCos flattened_kind co1 orig_kind unflattened_tys
             casted_args           = ASSERT2( equalLength args arg_cos
                                            , ppr args $$ ppr arg_cos )
                                     [ (casted_xi, casted_co)
@@ -2892,7 +2900,6 @@ simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs
                -- ... -> k, that k will be substituted to perhaps reveal more
                -- binders.
             zapped_lc             = zapLiftingContext lc
-            Pair flattened_kind _ = co1_kind
             (bndrs, new_inner)    = splitPiTys flattened_kind
 
             (xis_out, cos_out, res_co_out)
diff --git a/compiler/types/Coercion.hs-boot b/compiler/types/Coercion.hs-boot
index eb5e81b819..42d09c120a 100644
--- a/compiler/types/Coercion.hs-boot
+++ b/compiler/types/Coercion.hs-boot
@@ -38,7 +38,7 @@ mkAxiomRuleCo :: CoAxiomRule -> [Coercion] -> Coercion
 isGReflCo :: Coercion -> Bool
 isReflCo :: Coercion -> Bool
 isReflexiveCo :: Coercion -> Bool
-decomposePiCos :: HasDebugCallStack => Coercion -> Pair Type -> [Type] -> ([Coercion], Coercion)
+decomposePiCos :: HasDebugCallStack => Kind -> Coercion -> Kind -> [Type] -> ([Coercion], Coercion)
 coVarKindsTypesRole :: HasDebugCallStack => CoVar -> (Kind, Kind, Type, Type, Role)
 coVarRole :: CoVar -> Role
 
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index be2f74c731..f9a439b0b1 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -545,7 +545,7 @@ Accordingly, by eliminating reflexive casts, splitTyConApp need not worry
 about outermost casts to uphold (EQ). Eliminating reflexive casts is done
 in mkCastTy.
 
-Unforunately, that's not the end of the story. Consider comparing
+Unfortunately, that's not the end of the story. Consider comparing
   (T a b c)      =?       (T a b |> (co -> <Type>)) (c |> co)
 These two types have the same kind (Type), but the left type is a TyConApp
 while the right type is not. To handle this case, we say that the right-hand
@@ -567,15 +567,27 @@ our (EQ) property.
 Lastly, in order to detect reflexive casts reliably, we must make sure not
 to have nested casts: we update (t |> co1 |> co2) to (t |> (co1 `TransCo` co2)).
 
-In sum, in order to uphold (EQ), we need the following three invariants:
+In sum, in order to uphold (EQ), we need the following four invariants:
+
+  (EQ1) No ((fun_ty |> co) arg_ty)
+        where kind(fun_ty) = k1 -> k2    and resultKind(co) = k3 -> k4
+        or    kind(fun_ty) = forall a.k1 and resultKind(co) = forall a.k2
+        In these cases we can push the coercion to give
+             (fun_ty (arg_ty |> co1)) |> co2
+          where co1, co2 are gotten from co
+        Upheld by Type.mkAppTy
+
+  (EQ2) No (ty |> co) where kind(ty) = resultKind(co)
+        In this case we can discard the coercion altogether
+        Upheld by Type.mCastTy
+
+  (EQ3) No nested CastTys, (ty |> co1 |> co2)
+        In this case we can combine the coercions
+        Upheld by Type.mCastTy
 
-  (EQ1) No decomposable CastTy to the left of an AppTy, where a decomposable
-        cast is one that relates either a FunTy to a FunTy or a
-        ForAllTy to a ForAllTy.
-  (EQ2) No reflexive casts in CastTy.
-  (EQ3) No nested CastTys.
   (EQ4) No CastTy over (ForAllTy (Bndr tyvar vis) body).
         See Note [Weird typing rule for ForAllTy] in Type.
+        Upheld by Type.mCastTy
 
 These invariants are all documented above, in the declaration for Type.
 
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 749578d78f..bb85b29b36 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -248,7 +248,7 @@ import {-# SOURCE #-} Coercion( mkNomReflCo, mkGReflCo, mkReflCo
                               , mkKindCo, mkSubCo, mkFunCo, mkAxiomInstCo
                               , decomposePiCos, coercionKind, coercionLKind
                               , coercionRKind, coercionType
-                              , isReflexiveCo, seqCo )
+                              , seqCo )
 
 -- others
 import Util
@@ -764,13 +764,24 @@ the test in repSplitAppTy_maybe, which applies throughout, because
 the other calls to splitAppTy are in Unify, which is also used by
 the type checker (e.g. when matching type-function equations).
 
+Note [mkAppTy subtleties]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+Very important: mkAppTy is responsible for upholding (EQ1) in
+Note [Respecting definitional equality] in TyCoRep.
+
+Specifically, to uphold (EQ1) we have work to do when doing
+   mkAppTy (fun_ty |>co) arg_ty
+Note, crucially, that we pass (typeKind fun_ty) to decomposePiCos
+rather than inputKind( co ); the two may differ during type inference
+See Note [The Purely Kinded Type Invariant (PKTI)] in TcHsType.
 -}
 
 -- | Applies a type to another, as in e.g. @k a@
 mkAppTy :: Type -> Type -> Type
-  -- See Note [Respecting definitional equality], invariant (EQ1).
+-- See Note [mkAppTy subtleties]
 mkAppTy (CastTy fun_ty co) arg_ty
-  | ([arg_co], res_co) <- decomposePiCos co (coercionKind co) [arg_ty]
+  | ([arg_co], res_co) <- decomposePiCos (typeKind fun_ty) co
+                                         (pSnd $ coercionKind co) [arg_ty]
   = (fun_ty `mkAppTy` (arg_ty `mkCastTy` arg_co)) `mkCastTy` res_co
 
 mkAppTy (TyConApp tc tys) ty2 = mkTyConApp tc (tys ++ [ty2])
@@ -789,16 +800,18 @@ mkAppTy ty1               ty2 = AppTy ty1 ty2
         --   (T t1), (T t1 t2), etc
 
 mkAppTys :: Type -> [Type] -> Type
-mkAppTys ty1                []   = ty1
-mkAppTys (CastTy fun_ty co) arg_tys  -- much more efficient then nested mkAppTy
-                                     -- Why do this? See (EQ1) of
-                                     -- Note [Respecting definitional equality]
-                                     -- in TyCoRep
-  = foldl' AppTy ((mkAppTys fun_ty casted_arg_tys) `mkCastTy` res_co) leftovers
+mkAppTys ty1 []   = ty1
+
+mkAppTys (CastTy fun_ty co) arg_tys
+  = -- Much more efficient then nested mkAppTy
+    -- But see Note [mkAppTy subtleties]
+    foldl' AppTy ((mkAppTys fun_ty casted_arg_tys) `mkCastTy` res_co) leftovers
   where
-    (arg_cos, res_co) = decomposePiCos co (coercionKind co) arg_tys
+    (arg_cos, res_co) = decomposePiCos (typeKind fun_ty) co
+                                       (pSnd $ coercionKind co) arg_tys
     (args_to_cast, leftovers) = splitAtList arg_cos arg_tys
     casted_arg_tys = zipWith mkCastTy args_to_cast arg_cos
+
 mkAppTys (TyConApp tc tys1) tys2 = mkTyConApp tc (tys1 ++ tys2)
 mkAppTys ty1                tys2 = foldl' AppTy ty1 tys2
 
@@ -1316,16 +1329,41 @@ splitCastTy_maybe ty | Just ty' <- coreView ty = splitCastTy_maybe ty'
 splitCastTy_maybe (CastTy ty co)               = Just (ty, co)
 splitCastTy_maybe _                            = Nothing
 
--- | Make a 'CastTy'. The Coercion must be nominal. Checks the
--- Coercion for reflexivity, dropping it if it's reflexive.
--- See Note [Respecting definitional equality] in TyCoRep
+
+{- Note [mkCastTy subtleties]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Super important: mkCastTy is responsible for maintaining invariants
+(EQ2-4) in Note [Respecting definitional equality] in TyCoRep.
+See also Note [mkAppTy subtleties].
+
+Specifically
+
+* EQ2: we must to a full `eqType` check her. This is important to keep
+  the splitXXX functions working properly. Otherwise we may end up
+  with something like
+      (((->) |> something_reflexive_but_not_obviously_so) biz baz)
+  which fails under splitFunTy_maybe. This happened with the cheaper check
+  in test dependent/should_compile/dynamic-paper.
+  See Note [Respecting definitional equality] in TyCoRep
+
+* EQ2: crucially, note that we do /not/ use isReflexiveCo,
+  because during type inference the kind of 'ty' may be less
+  zonked than the input kind of the coercion.  See
+   Note [The Purely Kinded Type Invariant (PKTI)] in TcHsType
+
+* EQ3 (cast of cast) is easy
+
+* EQ3 (cast of forall) is reasonably easy
+-}
+
+-- | Make a 'CastTy'. The Coercion must be nominal.
+-- Some very important subtleties here: see Note [mkCastTy]
 mkCastTy :: Type -> Coercion -> Type
-mkCastTy ty co | isReflexiveCo co = ty  -- (EQ2) from the Note
--- NB: Do the slow check here. This is important to keep the splitXXX
--- functions working properly. Otherwise, we may end up with something
--- like (((->) |> something_reflexive_but_not_obviously_so) biz baz)
--- fails under splitFunTy_maybe. This happened with the cheaper check
--- in test dependent/should_compile/dynamic-paper.
+mkCastTy ty co
+  | let co_res_kind = pSnd (coercionKind co)
+  , typeKind ty `eqType` co_res_kind     -- (EQ2) from the Note
+    -- Not isReflexiveCo!  See Note [mkCastTy subtleties]
+  = ty
 
 mkCastTy (CastTy ty co1) co2
   -- (EQ3) from the Note
diff --git a/testsuite/tests/typecheck/should_fail/T16627.stderr b/testsuite/tests/typecheck/should_fail/T16627.stderr
index 108e99f44a..d66122f342 100644
--- a/testsuite/tests/typecheck/should_fail/T16627.stderr
+++ b/testsuite/tests/typecheck/should_fail/T16627.stderr
@@ -1,6 +1,8 @@
 
 T16627.hs:11:15: error:
-    • No instance for (Typeable r1) arising from a use of ‘typeRep’
+    • No instance for (Typeable (->)) arising from a use of ‘typeRep’
+        GHC can't yet do polykinded
+          Typeable ((->) :: TYPE r1 -> TYPE r2 -> *)
     • In the first argument of ‘mkTrApp’, namely ‘typeRep’
       In the first argument of ‘mkTrApp’, namely ‘typeRep `mkTrApp` a’
       In the expression: typeRep `mkTrApp` a `mkTrApp` b