Use NHsCoreTy to embed types into GND-generated codewip/use-NHsCoreTy-in-GND

`GeneralizedNewtypeDeriving` is in the unique situation where it must
produce an `LHsType GhcPs` from a Core `Type`. Historically, this was
done with the `typeToLHsType` function, which walked over the entire
`Type` and attempted to construct an `LHsType` with the same overall
structure. `typeToLHsType` is quite complicated, however, and has
been the subject of numerous bugs over the years (e.g., #14579).

Luckily, there is an easier way to accomplish the same thing: the
`XHsType` constructor of `HsType`. `XHsType` bundles an `NHsCoreTy`,
which allows embedding a Core `Type` directly into an `HsType`,
avoiding the need to laboriously convert from one to another (as
`typeToLHsType` did). Moreover, renaming and typechecking an
`XHsType` is simple, since one doesn't need to do anything to a
Core `Type`...

...well, almost. For the reasons described in
`Note [Typechecking NHsCoreTys]` in `GHC.Tc.Gen.HsType`, we must
apply a substitution that we build from the local `tcl_env` type
environment. But that's a relatively modest price to pay.

Now that `GeneralizedNewtypeDeriving` uses `NHsCoreTy`, the
`typeToLHsType` function no longer has any uses in GHC, so this patch
rips it out. Some additional tweaks to `hsTypeNeedsParens` were
necessary to make the new `-ddump-deriv` output correctly
parenthesized, but other than that, this patch is quite
straightforward.

This is a mostly internal refactoring, although it is likely that
`GeneralizedNewtypeDeriving`-generated code will now need fewer
language extensions in certain situations than it did before.

10 files changed, 148 insertions, 225 deletions

diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 3f3a728824..680ce67bc7 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -3040,7 +3040,7 @@ There are a couple of places in GHC where we convert Core Types into forms that
 more closely resemble user-written syntax. These include:
 
 1. Template Haskell Type reification (see, for instance, GHC.Tc.Gen.Splice.reify_tc_app)
-2. Converting Types to LHsTypes (in GHC.Hs.Utils.typeToLHsType, or in Haddock)
+2. Converting Types to LHsTypes (such as in Haddock.Convert in haddock)
 
 This conversion presents a challenge: how do we ensure that the resulting type
 has enough kind information so as not to be ambiguous? To better motivate this
@@ -3080,8 +3080,8 @@ require a kind signature? It might require it when we need to fill in any of
 T's omitted arguments. By "omitted argument", we mean one that is dropped when
 reifying ty_1 ... ty_n. Sometimes, the omitted arguments are inferred and
 specified arguments (e.g., TH reification in GHC.Tc.Gen.Splice), and sometimes the
-omitted arguments are only the inferred ones (e.g., in GHC.Hs.Utils.typeToLHsType,
-which reifies specified arguments through visible kind application).
+omitted arguments are only the inferred ones (e.g., in situations where
+specified arguments are reified through visible kind application).
 Regardless, the key idea is that _some_ arguments are going to be omitted after
 reification, and the only mechanism we have at our disposal for filling them in
 is through explicit kind signatures.
@@ -3178,7 +3178,7 @@ each form of tycon binder:
     injective_vars_of_binder(forall a. ...) = {a}.)
 
     There are some situations where using visible kind application is appropriate
-    (e.g., GHC.Hs.Utils.typeToLHsType) and others where it is not (e.g., TH
+    and others where it is not (e.g., TH
     reification), so the `injective_vars_of_binder` function is parametrized by
     a Bool which decides if specified binders should be counted towards
     injective positions or not.
diff --git a/compiler/GHC/Hs/Type.hs b/compiler/GHC/Hs/Type.hs
index ccf98857f4..c475357807 100644
--- a/compiler/GHC/Hs/Type.hs
+++ b/compiler/GHC/Hs/Type.hs
@@ -95,6 +95,7 @@ import GHC.Types.Name( Name, NamedThing(getName) )
 import GHC.Types.Name.Reader ( RdrName )
 import GHC.Core.DataCon( HsSrcBang(..), HsImplBang(..),
                          SrcStrictness(..), SrcUnpackedness(..) )
+import GHC.Core.TyCo.Rep ( Type(..) )
 import GHC.Builtin.Types( manyDataConName, oneDataConName, mkTupleStr )
 import GHC.Core.Type
 import GHC.Hs.Doc
@@ -866,6 +867,8 @@ data HsType pass
 data NewHsTypeX
   = NHsCoreTy Type -- An escape hatch for tunnelling a *closed*
                    -- Core Type through HsSyn.
+                   -- See also Note [Typechecking NHsCoreTys] in
+                   -- GHC.Tc.Gen.HsType.
     deriving Data
       -- ^ - 'GHC.Parser.Annotation.AnnKeywordId' : None
 
@@ -1870,32 +1873,43 @@ ppr_tylit (HsStrTy _ s) = text (show s)
 
 -- | @'hsTypeNeedsParens' p t@ returns 'True' if the type @t@ needs parentheses
 -- under precedence @p@.
-hsTypeNeedsParens :: PprPrec -> HsType pass -> Bool
-hsTypeNeedsParens p = go
+hsTypeNeedsParens :: PprPrec -> HsType (GhcPass p) -> Bool
+hsTypeNeedsParens p = go_hs_ty
   where
-    go (HsForAllTy{})        = p >= funPrec
-    go (HsQualTy{})          = p >= funPrec
-    go (HsBangTy{})          = p > topPrec
-    go (HsRecTy{})           = False
-    go (HsTyVar{})           = False
-    go (HsFunTy{})           = p >= funPrec
-    go (HsTupleTy{})         = False
-    go (HsSumTy{})           = False
-    go (HsKindSig{})         = p >= sigPrec
-    go (HsListTy{})          = False
-    go (HsIParamTy{})        = p > topPrec
-    go (HsSpliceTy{})        = False
-    go (HsExplicitListTy{})  = False
-    go (HsExplicitTupleTy{}) = False
-    go (HsTyLit{})           = False
-    go (HsWildCardTy{})      = False
-    go (HsStarTy{})          = p >= starPrec
-    go (HsAppTy{})           = p >= appPrec
-    go (HsAppKindTy{})       = p >= appPrec
-    go (HsOpTy{})            = p >= opPrec
-    go (HsParTy{})           = False
-    go (HsDocTy _ (L _ t) _) = go t
-    go (XHsType{})           = False
+    go_hs_ty (HsForAllTy{})           = p >= funPrec
+    go_hs_ty (HsQualTy{})             = p >= funPrec
+    go_hs_ty (HsBangTy{})             = p > topPrec
+    go_hs_ty (HsRecTy{})              = False
+    go_hs_ty (HsTyVar{})              = False
+    go_hs_ty (HsFunTy{})              = p >= funPrec
+    go_hs_ty (HsTupleTy{})            = False
+    go_hs_ty (HsSumTy{})              = False
+    go_hs_ty (HsKindSig{})            = p >= sigPrec
+    go_hs_ty (HsListTy{})             = False
+    go_hs_ty (HsIParamTy{})           = p > topPrec
+    go_hs_ty (HsSpliceTy{})           = False
+    go_hs_ty (HsExplicitListTy{})     = False
+    go_hs_ty (HsExplicitTupleTy{})    = False
+    go_hs_ty (HsTyLit{})              = False
+    go_hs_ty (HsWildCardTy{})         = False
+    go_hs_ty (HsStarTy{})             = p >= starPrec
+    go_hs_ty (HsAppTy{})              = p >= appPrec
+    go_hs_ty (HsAppKindTy{})          = p >= appPrec
+    go_hs_ty (HsOpTy{})               = p >= opPrec
+    go_hs_ty (HsParTy{})              = False
+    go_hs_ty (HsDocTy _ (L _ t) _)    = go_hs_ty t
+    go_hs_ty (XHsType (NHsCoreTy ty)) = go_core_ty ty
+
+    go_core_ty (TyVarTy{})    = False
+    go_core_ty (AppTy{})      = p >= appPrec
+    go_core_ty (TyConApp _ args)
+      | null args             = False
+      | otherwise             = p >= appPrec
+    go_core_ty (ForAllTy{})   = p >= funPrec
+    go_core_ty (FunTy{})      = p >= funPrec
+    go_core_ty (LitTy{})      = False
+    go_core_ty (CastTy t _)   = go_core_ty t
+    go_core_ty (CoercionTy{}) = False
 
 maybeAddSpace :: [LHsType pass] -> SDoc -> SDoc
 -- See Note [Printing promoted type constructors]
diff --git a/compiler/GHC/Hs/Utils.hs b/compiler/GHC/Hs/Utils.hs
index 1c8023946c..626a771be7 100644
--- a/compiler/GHC/Hs/Utils.hs
+++ b/compiler/GHC/Hs/Utils.hs
@@ -47,7 +47,6 @@ module GHC.Hs.Utils(
   nlHsIntLit, nlHsVarApps,
   nlHsDo, nlHsOpApp, nlHsLam, nlHsPar, nlHsIf, nlHsCase, nlList,
   mkLHsTupleExpr, mkLHsVarTuple, missingTupArg,
-  typeToLHsType,
 
   -- * Constructing general big tuples
   -- $big_tuples
@@ -119,9 +118,7 @@ import GHC.Tc.Types.Evidence
 import GHC.Types.Name.Reader
 import GHC.Types.Var
 import GHC.Core.TyCo.Rep
-import GHC.Core.TyCon
-import GHC.Core.Type ( appTyArgFlags, splitAppTys, tyConArgFlags, tyConAppNeedsKindSig )
-import GHC.Core.Multiplicity ( pattern One, pattern Many )
+import GHC.Core.Multiplicity ( pattern Many )
 import GHC.Builtin.Types ( unitTy )
 import GHC.Tc.Utils.TcType
 import GHC.Core.DataCon
@@ -680,139 +677,6 @@ mkClassOpSigs sigs
       = L loc (ClassOpSig noExtField False nms (dropWildCards ty))
     fiddle sig = sig
 
-typeToLHsType :: Type -> LHsType GhcPs
--- ^ Converting a Type to an HsType RdrName
--- This is needed to implement GeneralizedNewtypeDeriving.
---
--- Note that we use 'getRdrName' extensively, which
--- generates Exact RdrNames rather than strings.
-typeToLHsType ty
-  = go ty
-  where
-    go :: Type -> LHsType GhcPs
-    go ty@(FunTy { ft_af = af, ft_mult = mult, ft_arg = arg, ft_res = res })
-      = case af of
-          VisArg   -> nlHsFunTy (multToHsArrow mult) (go arg) (go res)
-          InvisArg | (theta, tau) <- tcSplitPhiTy ty
-                   -> noLoc (HsQualTy { hst_ctxt = noLoc (map go theta)
-                                      , hst_xqual = noExtField
-                                      , hst_body = go tau })
-
-    go ty@(ForAllTy (Bndr _ argf) _)
-      = noLoc (HsForAllTy { hst_tele = tele
-                          , hst_xforall = noExtField
-                          , hst_body = go tau })
-      where
-        (tele, tau)
-          | isVisibleArgFlag argf
-          = let (req_tvbs, tau') = tcSplitForAllTysReq ty in
-            (mkHsForAllVisTele (map go_tv req_tvbs), tau')
-          | otherwise
-          = let (inv_tvbs, tau') = tcSplitForAllTysInvis ty in
-            (mkHsForAllInvisTele (map go_tv inv_tvbs), tau')
-    go (TyVarTy tv)         = nlHsTyVar (getRdrName tv)
-    go (LitTy (NumTyLit n))
-      = noLoc $ HsTyLit noExtField (HsNumTy NoSourceText n)
-    go (LitTy (StrTyLit s))
-      = noLoc $ HsTyLit noExtField (HsStrTy NoSourceText s)
-    go ty@(TyConApp tc args)
-      | tyConAppNeedsKindSig True tc (length args)
-        -- We must produce an explicit kind signature here to make certain
-        -- programs kind-check. See Note [Kind signatures in typeToLHsType].
-      = nlHsParTy $ noLoc $ HsKindSig noExtField ty' (go (tcTypeKind ty))
-      | otherwise = ty'
-       where
-        ty' :: LHsType GhcPs
-        ty' = go_app (noLoc $ HsTyVar noExtField prom $ noLoc $ getRdrName tc)
-                     args (tyConArgFlags tc args)
-
-        prom :: PromotionFlag
-        prom = if isPromotedDataCon tc then IsPromoted else NotPromoted
-    go ty@(AppTy {})        = go_app (go head) args (appTyArgFlags head args)
-      where
-        head :: Type
-        args :: [Type]
-        (head, args) = splitAppTys ty
-    go (CastTy ty _)        = go ty
-    go (CoercionTy co)      = pprPanic "typeToLHsType" (ppr co)
-
-         -- Source-language types have _invisible_ kind arguments,
-         -- so we must remove them here (#8563)
-
-    go_app :: LHsType GhcPs -- The type being applied
-           -> [Type]        -- The argument types
-           -> [ArgFlag]     -- The argument types' visibilities
-           -> LHsType GhcPs
-    go_app head args arg_flags =
-      foldl' (\f (arg, flag) ->
-               let arg' = go arg in
-               case flag of
-                 -- See Note [Explicit Case Statement for Specificity]
-                 Invisible spec -> case spec of
-                   InferredSpec  -> f
-                   SpecifiedSpec -> f `nlHsAppKindTy` arg'
-                 Required  -> f `nlHsAppTy`     arg')
-             head (zip args arg_flags)
-
-    go_tv :: VarBndr TyVar flag -> LHsTyVarBndr flag GhcPs
-    go_tv (Bndr tv flag) = noLoc $ KindedTyVar noExtField
-                                               flag
-                                               (noLoc (getRdrName tv))
-                                               (go (tyVarKind tv))
-
--- | This is used to transform an arrow from Core's Type to surface
--- syntax. There is a choice between being very explicit here, or trying to
--- refold arrows into shorthands as much as possible. We choose to do the
--- latter, for it should be more readable. It also helps printing Haskell'98
--- code into Haskell'98 syntax.
-multToHsArrow :: Mult -> HsArrow GhcPs
-multToHsArrow One = HsLinearArrow
-multToHsArrow Many = HsUnrestrictedArrow
-multToHsArrow ty = HsExplicitMult (typeToLHsType ty)
-
-{-
-Note [Kind signatures in typeToLHsType]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-There are types that typeToLHsType can produce which require explicit kind
-signatures in order to kind-check. Here is an example from #14579:
-
-  -- type P :: forall {k} {t :: k}. Proxy t
-  type P = 'Proxy
-
-  -- type Wat :: forall a. Proxy a -> *
-  newtype Wat (x :: Proxy (a :: Type)) = MkWat (Maybe a)
-    deriving Eq
-
-  -- type Wat2 :: forall {a}. Proxy a -> *
-  type Wat2 = Wat
-
-  -- type Glurp :: * -> *
-  newtype Glurp a = MkGlurp (Wat2 (P :: Proxy a))
-    deriving Eq
-
-The derived Eq instance for Glurp (without any kind signatures) would be:
-
-  instance Eq a => Eq (Glurp a) where
-    (==) :: Glurp a -> Glurp a -> Bool
-    (==) = coerce @(Wat2 P  -> Wat2 P  -> Bool)
-                  @(Glurp a -> Glurp a -> Bool)
-                  (==)
-
-(Where the visible type applications use types produced by typeToLHsType.)
-
-The type P (in Wat2 P) has an underspecified kind, so we must ensure that
-typeToLHsType ascribes it with its kind: Wat2 (P :: Proxy a). To accomplish
-this, whenever we see an application of a tycon to some arguments, we use
-the tyConAppNeedsKindSig function to determine if it requires an explicit kind
-signature to resolve some ambiguity. (See Note
-Note [When does a tycon application need an explicit kind signature?] for a
-more detailed explanation of how this works.)
-
-Note that we pass True to tyConAppNeedsKindSig since we are generated code with
-visible kind applications, so even specified arguments count towards injective
-positions in the kind of the tycon.
--}
-
 {- *********************************************************************
 *                                                                      *
     --------- HsWrappers: type args, dict args, casts ---------
diff --git a/compiler/GHC/Tc/Deriv/Generate.hs b/compiler/GHC/Tc/Deriv/Generate.hs
index 1fe58c0414..135c7cd2ab 100644
--- a/compiler/GHC/Tc/Deriv/Generate.hs
+++ b/compiler/GHC/Tc/Deriv/Generate.hs
@@ -529,7 +529,7 @@ unliftedCompare lt_op eq_op a_expr b_expr lt eq gt
                         -- mean more tests (dynamically)
         nlHsIf (ascribeBool $ genPrimOpApp a_expr eq_op b_expr) eq gt
   where
-    ascribeBool e = nlExprWithTySig e boolTy
+    ascribeBool e = nlExprWithTySig e $ nlHsTyVar boolTyCon_RDR
 
 nlConWildPat :: DataCon -> LPat GhcPs
 -- The pattern (K {})
@@ -1855,7 +1855,7 @@ gen_Newtype_binds loc cls inst_tvs inst_tys rhs_ty
           --
           --   op :: forall c. a -> [T x] -> c -> Int
           L loc $ ClassOpSig noExtField False [loc_meth_RDR]
-                $ mkLHsSigType $ typeToLHsType to_ty
+                $ mkLHsSigType $ nlHsCoreTy to_ty
         )
       where
         Pair from_ty to_ty = mkCoerceClassMethEqn cls inst_tvs inst_tys rhs_ty meth_id
@@ -1911,12 +1911,15 @@ gen_Newtype_binds loc cls inst_tvs inst_tys rhs_ty
 nlHsAppType :: LHsExpr GhcPs -> Type -> LHsExpr GhcPs
 nlHsAppType e s = noLoc (HsAppType noExtField e hs_ty)
   where
-    hs_ty = mkHsWildCardBndrs $ parenthesizeHsType appPrec (typeToLHsType s)
+    hs_ty = mkHsWildCardBndrs $ parenthesizeHsType appPrec $ nlHsCoreTy s
 
-nlExprWithTySig :: LHsExpr GhcPs -> Type -> LHsExpr GhcPs
+nlExprWithTySig :: LHsExpr GhcPs -> LHsType GhcPs -> LHsExpr GhcPs
 nlExprWithTySig e s = noLoc $ ExprWithTySig noExtField (parenthesizeHsExpr sigPrec e) hs_ty
   where
-    hs_ty = mkLHsSigWcType (typeToLHsType s)
+    hs_ty = mkLHsSigWcType s
+
+nlHsCoreTy :: Type -> LHsType GhcPs
+nlHsCoreTy = noLoc . XHsType . NHsCoreTy
 
 mkCoerceClassMethEqn :: Class   -- the class being derived
                      -> [TyVar] -- the tvs in the instance head (this includes
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 68d29f565e..22edf3c0b4 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -90,6 +90,7 @@ import GHC.Tc.Utils.TcType
 import GHC.Tc.Utils.Instantiate ( tcInstInvisibleTyBinders, tcInstInvisibleTyBinder )
 import GHC.Core.Type
 import GHC.Builtin.Types.Prim
+import GHC.Types.Name.Env
 import GHC.Types.Name.Reader( lookupLocalRdrOcc )
 import GHC.Types.Var
 import GHC.Types.Var.Set
@@ -106,6 +107,7 @@ import GHC.Types.SrcLoc
 import GHC.Settings.Constants ( mAX_CTUPLE_SIZE )
 import GHC.Utils.Error( MsgDoc )
 import GHC.Types.Unique
+import GHC.Types.Unique.FM
 import GHC.Types.Unique.Set
 import GHC.Utils.Misc
 import GHC.Types.Unique.Supply
@@ -833,8 +835,17 @@ tc_infer_hs_type mode (HsSpliceTy _ (HsSpliced _ _ (HsSplicedTy ty)))
   = tc_infer_hs_type mode ty
 
 tc_infer_hs_type mode (HsDocTy _ ty _) = tc_infer_lhs_type mode ty
-tc_infer_hs_type _    (XHsType (NHsCoreTy ty))
-  = return (ty, tcTypeKind ty)
+
+-- See Note [Typechecking NHsCoreTys]
+tc_infer_hs_type _ (XHsType (NHsCoreTy ty))
+  = do env <- getLclEnv
+       let subst_prs = [ (nm, tv)
+                       | ATyVar nm tv <- nameEnvElts (tcl_env env) ]
+           subst = mkTvSubst
+                     (mkInScopeSet $ mkVarSet $ map snd subst_prs)
+                     (listToUFM $ map (liftSnd mkTyVarTy) subst_prs)
+           ty' = substTy subst ty
+       return (ty', tcTypeKind ty')
 
 tc_infer_hs_type _ (HsExplicitListTy _ _ tys)
   | null tys  -- this is so that we can use visible kind application with '[]
@@ -847,6 +858,47 @@ tc_infer_hs_type mode other_ty
        ; ty' <- tc_hs_type mode other_ty kv
        ; return (ty', kv) }
 
+{-
+Note [Typechecking NHsCoreTys]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+NHsCoreTy is an escape hatch that allows embedding Core Types in HsTypes.
+As such, there's not much to be done in order to typecheck an NHsCoreTy,
+since it's already been typechecked to some extent. There is one thing that
+we must do, however: we must substitute the type variables from the tcl_env.
+To see why, consider GeneralizedNewtypeDeriving, which is one of the main
+clients of NHsCoreTy (example adapted from #14579):
+
+  newtype T a = MkT a deriving newtype Eq
+
+This will produce an InstInfo GhcPs that looks roughly like this:
+
+  instance forall a_1. Eq a_1 => Eq (T a_1) where
+    (==) = coerce @(  a_1 ->   a_1 -> Bool) -- The type within @(...) is an NHsCoreTy
+                  @(T a_1 -> T a_1 -> Bool) -- So is this
+                  (==)
+
+This is then fed into the renamer. Since all of the type variables in this
+InstInfo use Exact RdrNames, the resulting InstInfo GhcRn looks basically
+identical. Things get more interesting when the InstInfo is fed into the
+typechecker, however. GHC will first generate fresh skolems to instantiate
+the instance-bound type variables with. In the example above, we might generate
+the skolem a_2 and use that to instantiate a_1, which extends the local type
+environment (tcl_env) with [a_1 :-> a_2]. This gives us:
+
+  instance forall a_2. Eq a_2 => Eq (T a_2) where ...
+
+To ensure that the body of this instance is well scoped, every occurrence of
+the `a` type variable should refer to a_2, the new skolem. However, the
+NHsCoreTys mention a_1, not a_2. Luckily, the tcl_env provides exactly the
+substitution we need ([a_1 :-> a_2]) to fix up the scoping. We apply this
+substitution to each NHsCoreTy and all is well:
+
+  instance forall a_2. Eq a_2 => Eq (T a_2) where
+    (==) = coerce @(  a_2 ->   a_2 -> Bool)
+                  @(T a_2 -> T a_2 -> Bool)
+                  (==)
+-}
+
 ------------------------------------------
 tcLHsType :: LHsType GhcRn -> TcKind -> TcM TcType
 tcLHsType hs_ty exp_kind
diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs
index dd828bc277..dc8aeb1962 100644
--- a/compiler/GHC/Tc/TyCl/Instance.hs
+++ b/compiler/GHC/Tc/TyCl/Instance.hs
@@ -1604,7 +1604,7 @@ tcMethods dfun_id clas tyvars dfun_ev_vars inst_tys
                -> TcM (TcId, LHsBind GhcTc, Maybe Implication)
 
     tc_default sel_id (Just (dm_name, _))
-      = do { (meth_bind, inline_prags) <- mkDefMethBind clas inst_tys sel_id dm_name
+      = do { (meth_bind, inline_prags) <- mkDefMethBind dfun_id clas sel_id dm_name
            ; tcMethodBody clas tyvars dfun_ev_vars inst_tys
                           dfun_ev_binds is_derived hs_sig_fn
                           spec_inst_prags inline_prags
@@ -1947,7 +1947,7 @@ mk_meth_spec_prags meth_id spec_inst_prags spec_prags_for_me
          | L inst_loc (SpecPrag _       wrap inl) <- spec_inst_prags]
 
 
-mkDefMethBind :: Class -> [Type] -> Id -> Name
+mkDefMethBind :: DFunId -> Class -> Id -> Name
               -> TcM (LHsBind GhcRn, [LSig GhcRn])
 -- The is a default method (vanailla or generic) defined in the class
 -- So make a binding   op = $dmop @t1 @t2
@@ -1955,7 +1955,7 @@ mkDefMethBind :: Class -> [Type] -> Id -> Name
 -- and t1,t2 are the instance types.
 -- See Note [Default methods in instances] for why we use
 -- visible type application here
-mkDefMethBind clas inst_tys sel_id dm_name
+mkDefMethBind dfun_id clas sel_id dm_name
   = do  { dflags <- getDynFlags
         ; dm_id <- tcLookupId dm_name
         ; let inline_prag = idInlinePragma dm_id
@@ -1980,6 +1980,8 @@ mkDefMethBind clas inst_tys sel_id dm_name
 
        ; return (bind, inline_prags) }
   where
+    (_, _, _, inst_tys) = tcSplitDFunTy (idType dfun_id)
+
     mk_vta :: LHsExpr GhcRn -> Type -> LHsExpr GhcRn
     mk_vta fun ty = noLoc (HsAppType noExtField fun (mkEmptyWildCardBndrs $ nlHsParTy
                                                 $ noLoc $ XHsType $ NHsCoreTy ty))
diff --git a/testsuite/tests/deriving/should_compile/T14578.stderr b/testsuite/tests/deriving/should_compile/T14578.stderr
index 58376989db..0018ebe569 100644
--- a/testsuite/tests/deriving/should_compile/T14578.stderr
+++ b/testsuite/tests/deriving/should_compile/T14578.stderr
@@ -9,18 +9,20 @@ Derived class instances:
     GHC.Base.sconcat ::
       GHC.Base.NonEmpty (T14578.Wat f g a) -> T14578.Wat f g a
     GHC.Base.stimes ::
-      forall (b :: TYPE 'GHC.Types.LiftedRep).
-      GHC.Real.Integral b => b -> T14578.Wat f g a -> T14578.Wat f g a
+      forall b.
+      GHC.Real.Integral b =>
+      b -> T14578.Wat f g a -> T14578.Wat f g a
     (GHC.Base.<>)
       = GHC.Prim.coerce
           @(T14578.App (Data.Functor.Compose.Compose f g) a
             -> T14578.App (Data.Functor.Compose.Compose f g) a
-               -> T14578.App (Data.Functor.Compose.Compose f g) a)
+            -> T14578.App (Data.Functor.Compose.Compose f g) a)
           @(T14578.Wat f g a -> T14578.Wat f g a -> T14578.Wat f g a)
           ((GHC.Base.<>) @(T14578.App (Data.Functor.Compose.Compose f g) a))
     GHC.Base.sconcat
       = GHC.Prim.coerce
-          @(GHC.Base.NonEmpty (T14578.App (Data.Functor.Compose.Compose f g) a)
+          @(GHC.Base.NonEmpty
+              (T14578.App (Data.Functor.Compose.Compose f g) a)
             -> T14578.App (Data.Functor.Compose.Compose f g) a)
           @(GHC.Base.NonEmpty (T14578.Wat f g a) -> T14578.Wat f g a)
           (GHC.Base.sconcat
@@ -29,7 +31,7 @@ Derived class instances:
       = GHC.Prim.coerce
           @(b
             -> T14578.App (Data.Functor.Compose.Compose f g) a
-               -> T14578.App (Data.Functor.Compose.Compose f g) a)
+            -> T14578.App (Data.Functor.Compose.Compose f g) a)
           @(b -> T14578.Wat f g a -> T14578.Wat f g a)
           (GHC.Base.stimes
              @(T14578.App (Data.Functor.Compose.Compose f g) a))
@@ -37,13 +39,8 @@ Derived class instances:
   instance GHC.Base.Functor f =>
            GHC.Base.Functor (T14578.App f) where
     GHC.Base.fmap ::
-      forall (a :: TYPE 'GHC.Types.LiftedRep)
-             (b :: TYPE 'GHC.Types.LiftedRep).
-      (a -> b) -> T14578.App f a -> T14578.App f b
-    (GHC.Base.<$) ::
-      forall (a :: TYPE 'GHC.Types.LiftedRep)
-             (b :: TYPE 'GHC.Types.LiftedRep).
-      a -> T14578.App f b -> T14578.App f a
+      forall a b. (a -> b) -> T14578.App f a -> T14578.App f b
+    (GHC.Base.<$) :: forall a b. a -> T14578.App f b -> T14578.App f a
     GHC.Base.fmap
       = GHC.Prim.coerce
           @((a -> b) -> f a -> f b)
@@ -55,25 +52,17 @@ Derived class instances:
   
   instance GHC.Base.Applicative f =>
            GHC.Base.Applicative (T14578.App f) where
-    GHC.Base.pure ::
-      forall (a :: TYPE 'GHC.Types.LiftedRep). a -> T14578.App f a
+    GHC.Base.pure :: forall a. a -> T14578.App f a
     (GHC.Base.<*>) ::
-      forall (a :: TYPE 'GHC.Types.LiftedRep)
-             (b :: TYPE 'GHC.Types.LiftedRep).
+      forall a b.
       T14578.App f (a -> b) -> T14578.App f a -> T14578.App f b
     GHC.Base.liftA2 ::
-      forall (a :: TYPE 'GHC.Types.LiftedRep)
-             (b :: TYPE 'GHC.Types.LiftedRep)
-             (c :: TYPE 'GHC.Types.LiftedRep).
+      forall a b c.
       (a -> b -> c) -> T14578.App f a -> T14578.App f b -> T14578.App f c
     (GHC.Base.*>) ::
-      forall (a :: TYPE 'GHC.Types.LiftedRep)
-             (b :: TYPE 'GHC.Types.LiftedRep).
-      T14578.App f a -> T14578.App f b -> T14578.App f b
+      forall a b. T14578.App f a -> T14578.App f b -> T14578.App f b
     (GHC.Base.<*) ::
-      forall (a :: TYPE 'GHC.Types.LiftedRep)
-             (b :: TYPE 'GHC.Types.LiftedRep).
-      T14578.App f a -> T14578.App f b -> T14578.App f a
+      forall a b. T14578.App f a -> T14578.App f b -> T14578.App f a
     GHC.Base.pure
       = GHC.Prim.coerce
           @(a -> f a) @(a -> T14578.App f a) (GHC.Base.pure @f)
@@ -105,15 +94,13 @@ Derived type family instances:
 
 
 ==================== Filling in method body ====================
-GHC.Base.Semigroup [T14578.App f[ssk:1] a[ssk:1]]
-  GHC.Base.sconcat = GHC.Base.$dmsconcat
-                       @(T14578.App f[ssk:1] a[ssk:1])
+GHC.Base.Semigroup [T14578.App f a]
+  GHC.Base.sconcat = GHC.Base.$dmsconcat @(T14578.App f a)
 
 
 
 ==================== Filling in method body ====================
-GHC.Base.Semigroup [T14578.App f[ssk:1] a[ssk:1]]
-  GHC.Base.stimes = GHC.Base.$dmstimes
-                      @(T14578.App f[ssk:1] a[ssk:1])
+GHC.Base.Semigroup [T14578.App f a]
+  GHC.Base.stimes = GHC.Base.$dmstimes @(T14578.App f a)
 
 
diff --git a/testsuite/tests/deriving/should_compile/T14579.stderr b/testsuite/tests/deriving/should_compile/T14579.stderr
index 81212022ef..31545c6de7 100644
--- a/testsuite/tests/deriving/should_compile/T14579.stderr
+++ b/testsuite/tests/deriving/should_compile/T14579.stderr
@@ -8,34 +8,36 @@ Derived class instances:
       T14579.Glurp a -> T14579.Glurp a -> GHC.Types.Bool
     (GHC.Classes.==)
       = GHC.Prim.coerce
-          @(T14579.Wat @a ('Data.Proxy.Proxy @a)
-            -> T14579.Wat @a ('Data.Proxy.Proxy @a) -> GHC.Types.Bool)
+          @(T14579.Wat 'Data.Proxy.Proxy
+            -> T14579.Wat 'Data.Proxy.Proxy -> GHC.Types.Bool)
           @(T14579.Glurp a -> T14579.Glurp a -> GHC.Types.Bool)
-          ((GHC.Classes.==) @(T14579.Wat @a ('Data.Proxy.Proxy @a)))
+          ((GHC.Classes.==) @(T14579.Wat 'Data.Proxy.Proxy))
     (GHC.Classes./=)
       = GHC.Prim.coerce
-          @(T14579.Wat @a ('Data.Proxy.Proxy @a)
-            -> T14579.Wat @a ('Data.Proxy.Proxy @a) -> GHC.Types.Bool)
+          @(T14579.Wat 'Data.Proxy.Proxy
+            -> T14579.Wat 'Data.Proxy.Proxy -> GHC.Types.Bool)
           @(T14579.Glurp a -> T14579.Glurp a -> GHC.Types.Bool)
-          ((GHC.Classes./=) @(T14579.Wat @a ('Data.Proxy.Proxy @a)))
+          ((GHC.Classes./=) @(T14579.Wat 'Data.Proxy.Proxy))
   
   instance forall a (x :: Data.Proxy.Proxy a).
            GHC.Classes.Eq a =>
            GHC.Classes.Eq (T14579.Wat x) where
     (GHC.Classes.==) ::
-      T14579.Wat @a x -> T14579.Wat @a x -> GHC.Types.Bool
+      T14579.Wat x[sk:1] -> T14579.Wat x[sk:1] -> GHC.Types.Bool
     (GHC.Classes./=) ::
-      T14579.Wat @a x -> T14579.Wat @a x -> GHC.Types.Bool
+      T14579.Wat x[sk:1] -> T14579.Wat x[sk:1] -> GHC.Types.Bool
     (GHC.Classes.==)
       = GHC.Prim.coerce
-          @(GHC.Maybe.Maybe a -> GHC.Maybe.Maybe a -> GHC.Types.Bool)
-          @(T14579.Wat @a x -> T14579.Wat @a x -> GHC.Types.Bool)
-          ((GHC.Classes.==) @(GHC.Maybe.Maybe a))
+          @(GHC.Maybe.Maybe a[sk:1]
+            -> GHC.Maybe.Maybe a[sk:1] -> GHC.Types.Bool)
+          @(T14579.Wat x[sk:1] -> T14579.Wat x[sk:1] -> GHC.Types.Bool)
+          ((GHC.Classes.==) @(GHC.Maybe.Maybe a[sk:1]))
     (GHC.Classes./=)
       = GHC.Prim.coerce
-          @(GHC.Maybe.Maybe a -> GHC.Maybe.Maybe a -> GHC.Types.Bool)
-          @(T14579.Wat @a x -> T14579.Wat @a x -> GHC.Types.Bool)
-          ((GHC.Classes./=) @(GHC.Maybe.Maybe a))
+          @(GHC.Maybe.Maybe a[sk:1]
+            -> GHC.Maybe.Maybe a[sk:1] -> GHC.Types.Bool)
+          @(T14579.Wat x[sk:1] -> T14579.Wat x[sk:1] -> GHC.Types.Bool)
+          ((GHC.Classes./=) @(GHC.Maybe.Maybe a[sk:1]))
   
 
 Derived type family instances:
diff --git a/testsuite/tests/deriving/should_fail/T15073.stderr b/testsuite/tests/deriving/should_fail/T15073.stderr
index 129efe496d..f39fd19bbc 100644
--- a/testsuite/tests/deriving/should_fail/T15073.stderr
+++ b/testsuite/tests/deriving/should_fail/T15073.stderr
@@ -2,8 +2,7 @@
 T15073.hs:8:12: error:
     • Illegal unboxed tuple type as function argument: (# Foo a #)
       Perhaps you intended to use UnboxedTuples
-    • In the type signature:
-        p :: Foo a -> Solo# @'GHC.Types.LiftedRep (Foo a)
+    • In the type signature: p :: Foo a -> (# Foo a #)
       When typechecking the code for ‘p’
         in a derived instance for ‘P (Foo a)’:
         To see the code I am typechecking, use -ddump-deriv
diff --git a/testsuite/tests/deriving/should_fail/deriving-via-fail5.stderr b/testsuite/tests/deriving/should_fail/deriving-via-fail5.stderr
index a0a19ab65d..497e955896 100644
--- a/testsuite/tests/deriving/should_fail/deriving-via-fail5.stderr
+++ b/testsuite/tests/deriving/should_fail/deriving-via-fail5.stderr
@@ -59,12 +59,12 @@ deriving-via-fail5.hs:8:1: error:
         at deriving-via-fail5.hs:(8,1)-(9,24)
     • In the expression:
         GHC.Prim.coerce
-          @([] (Identity b) -> ShowS) @([] (Foo4 a) -> ShowS)
+          @([Identity b] -> ShowS) @([Foo4 a] -> ShowS)
           (showList @(Identity b))
       In an equation for ‘showList’:
           showList
             = GHC.Prim.coerce
-                @([] (Identity b) -> ShowS) @([] (Foo4 a) -> ShowS)
+                @([Identity b] -> ShowS) @([Foo4 a] -> ShowS)
                 (showList @(Identity b))
       When typechecking the code for ‘showList’
         in a derived instance for ‘Show (Foo4 a)’: