WIP: 22478 Type patternswip/int-index/tyconpat-scoping

10 files changed, 320 insertions, 104 deletions

diff --git a/compiler/GHC/Hs/Pat.hs b/compiler/GHC/Hs/Pat.hs
index 39a788aab5..ed116a6acb 100644
--- a/compiler/GHC/Hs/Pat.hs
+++ b/compiler/GHC/Hs/Pat.hs
@@ -28,7 +28,7 @@ module GHC.Hs.Pat (
         HsPatExpansion(..),
         XXPatGhcTc(..),
 
-        HsConPatDetails, hsConPatArgs,
+        HsConPatDetails, hsConPatArgs, hsConPatTyArgs,
         HsConPatTyArg(..),
         HsRecFields(..), HsFieldBind(..), LHsFieldBind,
         HsRecField, LHsRecField,
diff --git a/compiler/GHC/Hs/Utils.hs b/compiler/GHC/Hs/Utils.hs
index af222bf98a..c7380990e9 100644
--- a/compiler/GHC/Hs/Utils.hs
+++ b/compiler/GHC/Hs/Utils.hs
@@ -1136,6 +1136,8 @@ data CollectFlag p where
     CollNoDictBinders   :: CollectFlag p
     -- | Collect evidence binders
     CollWithDictBinders :: CollectFlag GhcTc
+    -- | Collect variable and type variable binders, but no evidence binders
+    CollVarTyVarBinders :: CollectFlag GhcRn
 
 collect_lpat :: forall p. CollectPass p
              => CollectFlag p
@@ -1171,6 +1173,63 @@ collect_pat flag pat bndrs = case pat of
     CollNoDictBinders   -> foldr (collect_lpat flag) bndrs (hsConPatArgs ps)
     CollWithDictBinders -> foldr (collect_lpat flag) bndrs (hsConPatArgs ps)
                            ++ collectEvBinders (cpt_binds (pat_con_ext pat))
+    CollVarTyVarBinders ->
+      let { unwrapTyArg (HsConPatTyArg _ t) = hsps_body t
+          ; bndrs'  = foldr (collect_lpat flag) bndrs (hsConPatArgs ps)
+          ; bndrs'' = foldr (collect_ltypat . unwrapTyArg) bndrs' (hsConPatTyArgs ps)
+          } in bndrs''
+
+collect_ltypat :: LHsType GhcRn -> [Name] -> [Name]
+collect_ltypat ltypat = collect_typat (unLoc ltypat)
+
+collect_typat :: HsType GhcRn -> [Name] -> [Name]
+collect_typat typat bndrs = case typat of
+  HsTyVar _ _ (L _ name)
+    | isTyVarName name -> name : bndrs
+    | otherwise        -> bndrs
+  HsParTy _ t             -> collect_ltypat t bndrs
+  HsWildCardTy _          -> bndrs
+  HsAppTy _ t1 t2         -> collect_ltypat t1 (collect_ltypat t2 bndrs)
+  HsAppKindTy _ t1 _ t2   -> collect_ltypat t1 (collect_ltypat t2 bndrs)
+  HsOpTy _ _ t1 op t2     -> unLoc op : collect_ltypat t1 (collect_ltypat t2 bndrs)
+  HsQualTy _ (L _ ts) t   -> foldr collect_ltypat (collect_ltypat t bndrs) ts
+  HsFunTy _ arr t1 t2     -> collect_arr arr (collect_ltypat t1 (collect_ltypat t2 bndrs))
+  HsListTy _ t            -> collect_ltypat t bndrs
+  HsTupleTy _ _ ts        -> foldr collect_ltypat bndrs ts
+  HsSumTy _ ts            -> foldr collect_ltypat bndrs ts
+  HsExplicitListTy _ _ ts -> foldr collect_ltypat bndrs ts
+  HsExplicitTupleTy _ ts  -> foldr collect_ltypat bndrs ts
+  HsStarTy _ _            -> bndrs
+  HsKindSig _ t _         ->
+    -- Do not collect variables in the sig: they are usages, not bindings.
+    -- See ghc-proposals/pull/556
+    collect_ltypat t bndrs
+  HsForAllTy _ _ t        ->
+    -- Discard the telescope since it does not affect what variables are bound.
+    -- Consider:
+    --    f (MkT @(forall a. Maybe a)) = rhs
+    -- The "a" in "Maybe a" is *not* forall-bound, it is its own binding
+    -- that scopes outside the forall.
+    collect_ltypat t bndrs
+  HsBangTy _ _ t          -> collect_ltypat t bndrs
+  HsDocTy _ t _           -> collect_ltypat t bndrs
+  HsIParamTy _ _ t        -> collect_ltypat t bndrs
+  HsTyLit _ _             -> bndrs
+  HsSpliceTy _ _          -> bndrs    -- FIXME (int-index): reconsider after fixing the fSpliceTy example
+  HsRecTy{} ->
+    -- Not valid syntax in type patterns, but we need to return something
+    -- instead of panicking to let the type error (generated elsewhere) propagate.
+    bndrs
+  XHsType{} ->
+    -- XHsType at GhcRn is only produced by deriving, which never generates type patterns,
+    -- so this case is unreachable at the moment.
+    panic "collect_typat: XHsType"
+
+  where
+    collect_arr :: HsArrow GhcRn -> [Name] -> [Name]
+    collect_arr (HsUnrestrictedArrow _) = id
+    collect_arr (HsLinearArrow _) = id
+    collect_arr (HsExplicitMult _ t _) = collect_ltypat t
 
 collectEvBinders :: TcEvBinds -> [Id]
 collectEvBinders (EvBinds bs)   = foldr add_ev_bndr [] bs
diff --git a/compiler/GHC/Rename/HsType.hs b/compiler/GHC/Rename/HsType.hs
index f9720a53e1..521fc65f04 100644
--- a/compiler/GHC/Rename/HsType.hs
+++ b/compiler/GHC/Rename/HsType.hs
@@ -14,12 +14,13 @@ module GHC.Rename.HsType (
         -- Type related stuff
         rnHsType, rnLHsType, rnLHsTypes, rnContext, rnMaybeContext,
         rnLHsKind, rnLHsTypeArgs,
-        rnHsSigType, rnHsWcType, rnHsPatSigTypeBindingVars,
+        rnHsSigType, rnHsWcType,
         HsPatSigTypeScoping(..), rnHsSigWcType, rnHsPatSigType,
         newTyVarNameRn,
         rnConDeclFields,
         lookupField,
         rnLTyVar,
+        rnHsTyLit,
 
         rnScaledLHsType,
 
@@ -81,8 +82,6 @@ import qualified GHC.LanguageExtensions as LangExt
 import Language.Haskell.Syntax.Basic (FieldLabelString(..))
 
 import Data.List (nubBy, partition)
-import qualified Data.List.NonEmpty as NE
-import Data.List.NonEmpty (NonEmpty(..))
 import Control.Monad
 
 {-
@@ -185,57 +184,6 @@ rnHsWcType ctxt (HsWC { hswc_body = hs_ty })
        ; let sig_ty' = HsWC { hswc_ext = wcs, hswc_body = hs_ty' }
        ; return (sig_ty', fvs) }
 
--- Similar to rnHsWcType, but rather than requiring free variables in the type to
--- already be in scope, we are going to require them not to be in scope,
--- and we bind them.
-rnHsPatSigTypeBindingVars :: HsDocContext
-                          -> HsPatSigType GhcPs
-                          -> (HsPatSigType GhcRn -> RnM (r, FreeVars))
-                          -> RnM (r, FreeVars)
-rnHsPatSigTypeBindingVars ctxt sigType thing_inside = case sigType of
-  (HsPS { hsps_body = hs_ty }) -> do
-    rdr_env <- getLocalRdrEnv
-    let (varsInScope, varsNotInScope) =
-          partition (inScope rdr_env . unLoc) (extractHsTyRdrTyVars hs_ty)
-    -- TODO: Resolve and remove this comment.
-    -- This next bit is in some contention. The original proposal #126
-    -- (https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0126-type-applications-in-patterns.rst)
-    -- says that in-scope variables are fine here: don't bind them, just use
-    -- the existing vars, like in type signatures. An amendment #291
-    -- (https://github.com/ghc-proposals/ghc-proposals/pull/291) says that the
-    -- use of an in-scope variable should *shadow* an in-scope tyvar, like in
-    -- terms. In an effort to make forward progress, the current implementation
-    -- just rejects any use of an in-scope variable, meaning GHC will accept
-    -- a subset of programs common to both variants. If this comment still exists
-    -- in mid-to-late 2021 or thereafter, we have done a poor job on following
-    -- up on this point.
-    -- Example:
-    --   f :: forall a. ...
-    --   f (MkT @a ...) = ...
-    -- Should the inner `a` refer to the outer one? shadow it? We are, as yet, undecided,
-    -- so we currently reject.
-    when (not (null varsInScope)) $
-      addErr $ mkTcRnUnknownMessage $ mkPlainError noHints $
-        vcat
-          [ text "Type variable" <> plural varsInScope
-            <+> hcat (punctuate (text ",") (map (quotes . ppr) varsInScope))
-            <+> isOrAre varsInScope
-            <+> text "already in scope."
-          , text "Type applications in patterns must bind fresh variables, without shadowing."
-          ]
-    (wcVars, ibVars) <- partition_nwcs varsNotInScope
-    rnImplicitTvBndrs ctxt Nothing ibVars $ \ ibVars' -> do
-      (wcVars', hs_ty', fvs) <- rnWcBody ctxt wcVars hs_ty
-      let sig_ty = HsPS
-            { hsps_body = hs_ty'
-            , hsps_ext = HsPSRn
-              { hsps_nwcs    = wcVars'
-              , hsps_imp_tvs = ibVars'
-              }
-            }
-      (res, fvs') <- thing_inside sig_ty
-      return (res, fvs `plusFV` fvs')
-
 rnWcBody :: HsDocContext -> [LocatedN RdrName] -> LHsType GhcPs
          -> RnM ([Name], LHsType GhcRn, FreeVars)
 rnWcBody ctxt nwc_rdrs hs_ty
@@ -432,34 +380,6 @@ type signature, since the type signature implicitly carries their binding
 sites. This is less precise, but more accurate.
 -}
 
--- | Create fresh type variables for binders, disallowing multiple occurrences of the same variable. Similar to `rnImplicitTvOccs` except that duplicate occurrences will
--- result in an error, and the source locations of the variables are not adjusted, as these variable occurrences are themselves the binding sites for the type variables,
--- rather than the variables being implicitly bound by a signature.
-rnImplicitTvBndrs :: HsDocContext
-                  -> Maybe assoc
-                  -- ^ @'Just' _@ => an associated type decl
-                  -> FreeKiTyVars
-                  -- ^ Surface-syntax free vars that we will implicitly bind.
-                  -- Duplicate variables will cause a compile-time error regarding repeated bindings.
-                  -> ([Name] -> RnM (a, FreeVars))
-                  -> RnM (a, FreeVars)
-rnImplicitTvBndrs ctx mb_assoc implicit_vs_with_dups thing_inside
-  = do { implicit_vs <- forM (NE.groupAllWith unLoc $ implicit_vs_with_dups) $ \case
-           (x :| []) -> return x
-           (x :| _) -> do
-             let msg = mkTcRnUnknownMessage $ mkPlainError noHints $
-                   text "Variable" <+> text "`" <> ppr x <> text "'" <+> text "would be bound multiple times by" <+> pprHsDocContext ctx <> text "."
-             addErr msg
-             return x
-
-       ; traceRn "rnImplicitTvBndrs" $
-         vcat [ ppr implicit_vs_with_dups, ppr implicit_vs ]
-
-       ; vars <- mapM (newTyVarNameRn mb_assoc) implicit_vs
-
-       ; bindLocalNamesFV vars $
-         thing_inside vars }
-
 {- ******************************************************
 *                                                       *
            LHsType and HsType
diff --git a/compiler/GHC/Rename/Pat.hs b/compiler/GHC/Rename/Pat.hs
index 169c2e508c..1a7a82ccf7 100644
--- a/compiler/GHC/Rename/Pat.hs
+++ b/compiler/GHC/Rename/Pat.hs
@@ -53,7 +53,8 @@ import GHC.Rename.Utils    ( newLocalBndrRn, bindLocalNames
                            , warnUnusedMatches, newLocalBndrRn
                            , checkUnusedRecordWildcard
                            , checkDupNames, checkDupAndShadowedNames
-                           , wrapGenSpan, genHsApps, genLHsVar, genHsIntegralLit, warnForallIdentifier )
+                           , wrapGenSpan, genHsApps, genLHsVar, genHsIntegralLit, warnForallIdentifier
+                           , bindLocalNamesFV )
 import GHC.Rename.HsType
 import GHC.Builtin.Names
 import GHC.Types.Avail ( greNameMangledName )
@@ -75,8 +76,11 @@ import GHC.Driver.Session ( getDynFlags, xopt_DuplicateRecordFields )
 import qualified GHC.LanguageExtensions as LangExt
 
 import Control.Monad       ( when, ap, guard, unless )
+import Control.Monad.Trans.Class
+import Control.Monad.Trans.Writer.CPS
 import Data.Foldable
 import Data.Functor.Identity ( Identity (..) )
+import qualified Data.Semigroup as S
 import qualified Data.List.NonEmpty as NE
 import Data.Maybe
 import Data.Ratio
@@ -145,6 +149,14 @@ wrapSrcSpanCps fn (L loc a)
                  unCpsRn (fn a) $ \v ->
                  k (L loc v))
 
+wrapSrcSpanWriterCps :: Monoid w => (a -> WriterT w CpsRn b) -> LocatedAn ann a -> WriterT w CpsRn (LocatedAn ann b)
+wrapSrcSpanWriterCps fn (L loc a) =
+  mapWriterT
+    (\m -> CpsRn (\k -> setSrcSpanA loc $
+                        unCpsRn m $ \(v, acc) ->
+                        k (L loc v, acc)))
+    (fn a)
+
 lookupConCps :: LocatedN RdrName -> CpsRn (LocatedN Name)
 lookupConCps con_rdr
   = CpsRn (\k -> do { con_name <- lookupLocatedOccRnConstr con_rdr
@@ -424,7 +436,7 @@ rnPats ctxt pats thing_inside
           --    complain *twice* about duplicates e.g. f (x,x) = ...
           --
           -- See Note [Don't report shadowing for pattern synonyms]
-        ; let bndrs = collectPatsBinders CollNoDictBinders (toList pats')
+        ; let bndrs = collectPatsBinders CollVarTyVarBinders (toList pats')
         ; addErrCtxt doc_pat $
           if isPatSynCtxt ctxt
              then checkDupNames bndrs
@@ -649,7 +661,7 @@ rnConPatAndThen mk con (PrefixCon tyargs pats)
                     <+> quotes (ppr tyarg))
                2 (text "Perhaps you intended to use TypeAbstractions")
     rnConPatTyArg (HsConPatTyArg at t) = do
-      t' <- liftCpsWithCont $ rnHsPatSigTypeBindingVars HsTypeCtx t
+      t' <- rnHsTyPat t
       return (HsConPatTyArg at t')
 
 rnConPatAndThen mk con (InfixCon pat1 pat2)
@@ -711,6 +723,140 @@ rnHsRecPatsAndThen mk (L _ con)
     nested_mk (Just (unLoc -> n)) (LamMk report_unused) n'
       = LamMk (report_unused && (n' <= n))
 
+{- *********************************************************************
+*                                                                      *
+                         Type patterns
+*                                                                      *
+********************************************************************* -}
+
+data TyPatVarsAccum =
+  TyPatVarsAccum {
+    tpv_acc_nwcs    :: [Name] -> [Name], -- ^ Wildcard names
+    tpv_acc_exp_tvs :: [Name] -> [Name], -- ^ Explicitly bound variable names
+    tpv_acc_imp_tvs :: [Name] -> [Name]  -- ^ Implicitly bound variable names
+  }
+
+instance Semigroup TyPatVarsAccum where
+  TyPatVarsAccum a1 b1 c1 <> TyPatVarsAccum a2 b2 c2 =
+    TyPatVarsAccum (a1 S.<> a2) (b1 S.<> b2) (c1 S.<> c2)
+
+instance Monoid TyPatVarsAccum where
+  mempty = TyPatVarsAccum id id id
+
+tpv_HsPSRn :: TyPatVarsAccum -> HsPSRn
+tpv_HsPSRn (TyPatVarsAccum nwcs_acc exp_tvs_acc imp_tvs_acc) =
+  HsPSRn (nwcs_acc []) (exp_tvs_acc (imp_tvs_acc []))
+
+tpv_exp_tv :: Name -> TyPatVarsAccum
+tpv_exp_tv tv = mempty { tpv_acc_exp_tvs = (tv:) }
+
+tpv_sig_tvs :: HsPSRn -> TyPatVarsAccum
+tpv_sig_tvs (HsPSRn nwcs imp_tvs) =
+  mempty { tpv_acc_nwcs    = (nwcs++)
+         , tpv_acc_imp_tvs = (imp_tvs++) }
+
+rnHsTyPat :: HsPatSigType GhcPs -> CpsRn (HsPatSigType GhcRn)
+rnHsTyPat (HsPS _ hs_top_ty) =
+  do { (hs_top_ty', tpv_acc) <- runWriterT (go_lty hs_top_ty)
+     ; return (HsPS (tpv_HsPSRn tpv_acc) hs_top_ty') }
+  where
+    go_lty :: LHsType GhcPs -> WriterT TyPatVarsAccum CpsRn (LHsType GhcRn)
+    go_lty = wrapSrcSpanWriterCps go_ty
+
+    go_ty :: HsType GhcPs -> WriterT TyPatVarsAccum CpsRn (HsType GhcRn)
+    go_ty (HsTyVar _ prom lrdr) =
+      fmap (\lnm -> HsTyVar noAnn prom lnm)
+           (go_name prom lrdr)
+    go_ty (HsParTy _ t) =
+      do { t' <- go_lty t
+         ; return (HsParTy noAnn t') }
+    go_ty (HsWildCardTy _) = return (HsWildCardTy noExtField)
+    go_ty (HsAppTy _ ty1 ty2) =
+      do { ty1' <- go_lty ty1
+         ; ty2' <- go_lty ty2
+         ; return (HsAppTy noExtField ty1' ty2') }
+    go_ty (HsAppKindTy _ ty1 at ty2) =
+      do { ty1' <- go_lty ty1
+         ; ty2' <- go_lty ty2
+         ; return (HsAppKindTy noExtField ty1' at ty2') }
+    go_ty (HsOpTy _ prom ty1 op ty2) =
+      do { op' <- go_name prom op
+         ; ty1' <- go_lty ty1
+         ; ty2' <- go_lty ty2
+         ; return (HsOpTy noAnn prom ty1' op' ty2') }
+         -- FIXME (int-index): check operator fixity
+    go_ty (HsQualTy _ lctx t) =
+      do { lctx' <- wrapSrcSpanWriterCps (mapM go_lty) lctx
+         ; t' <- go_lty t
+         ; return (HsQualTy noExtField lctx' t') }
+    go_ty (HsFunTy u mult ty1 ty2) =
+      do { mult' <- go_arr mult
+         ; ty1' <- go_lty ty1
+         ; ty2' <- go_lty ty2
+         ; return (HsFunTy u mult' ty1' ty2') }
+    go_ty (HsListTy x t) =
+      do { t' <- go_lty t
+         ; return (HsListTy x t') }
+    go_ty (HsTupleTy x tup_con ts) =
+      do { ts' <- mapM go_lty ts
+         ; return (HsTupleTy x tup_con ts') }
+    go_ty (HsSumTy x ts) =
+      do { ts' <- mapM go_lty ts
+         ; return (HsSumTy x ts') }
+    go_ty (HsExplicitListTy _ prom ts) =
+      do { ts' <- mapM go_lty ts
+         ; return (HsExplicitListTy noExtField prom ts') }
+    go_ty (HsExplicitTupleTy _ ts) =
+      do { ts' <- mapM go_lty ts
+         ; return (HsExplicitTupleTy noExtField ts') }
+    go_ty (HsStarTy _ isUni) = return (HsStarTy noExtField isUni)
+    go_ty (HsKindSig x t k) =
+      do { k' <- go_lksig k
+         ; t' <- go_lty t
+         ; return (HsKindSig x t' k') }
+    go_ty (HsForAllTy _ _ _) = panic "rnHsTyPat: HsForAllTy"
+    go_ty (HsBangTy _ _ _) = panic "rnHsTyPat: HsBangTy"
+    go_ty (HsDocTy _ _ _) = panic "rnHsTyPat: HsDocTy"
+    go_ty (HsIParamTy x n t) =
+      do { t' <- go_lty t
+         ; return (HsIParamTy x n t') }
+    go_ty (HsTyLit src lit) = return (HsTyLit src (rnHsTyLit lit))
+    go_ty (HsSpliceTy _ _) = panic "rnHsTyPat: HsSpliceTy"
+    go_ty HsRecTy{} = panic "rnHsTyPat: HsRecTy"
+    go_ty XHsType{} =
+      -- XHsType at GhcRn is only produced by deriving, which never generates type patterns,
+      -- so this case is unreachable at the moment.
+      panic "rnHsTyPat: XHsType"
+
+    go_lksig :: LHsKind GhcPs -> WriterT TyPatVarsAccum CpsRn (LHsKind GhcRn)
+    go_lksig k =
+      do { sig' <- lift $ liftCpsWithCont $ rnHsPatSigType AlwaysBind PatCtx (HsPS noAnn k)
+         ; let !(HsPS x k') = sig'
+         ; writer (k', tpv_sig_tvs x) }
+
+    go_name :: PromotionFlag -> LIdP GhcPs -> WriterT TyPatVarsAccum CpsRn (LIdP GhcRn)
+    go_name _ lrdr
+      | isRdrTyVar (unLoc lrdr) = go_var lrdr    -- Type variable binding
+      | otherwise = lift $ liftCpsFV $           -- Type constructor usage
+          do { lnm@(L _ nm) <- rnLTyVar lrdr
+             ; return (lnm, unitFV nm) }
+
+    go_var :: LIdP GhcPs -> WriterT TyPatVarsAccum CpsRn (LIdP GhcRn)
+    go_var lrdr =
+      writerT $ liftCpsWithCont $ \thing_inside ->
+            do { nm <- newTyVarNameRn Nothing lrdr
+               ; let lnm = L (getLoc lrdr) nm
+               ; bindLocalNamesFV [nm] $
+                 thing_inside (lnm, tpv_exp_tv nm)
+               }
+
+    go_arr :: HsArrow GhcPs -> WriterT TyPatVarsAccum CpsRn (HsArrow GhcRn)
+    go_arr (HsUnrestrictedArrow arr) = return (HsUnrestrictedArrow arr)
+    go_arr (HsLinearArrow (HsPct1 pct1 arr)) = return (HsLinearArrow (HsPct1 pct1 arr))
+    go_arr (HsLinearArrow (HsLolly arr)) = return (HsLinearArrow (HsLolly arr))
+    go_arr (HsExplicitMult pct p arr) =
+      do { p' <- go_lty p
+         ; return (HsExplicitMult pct p' arr) }
 
 {- *********************************************************************
 *                                                                      *
diff --git a/compiler/Language/Haskell/Syntax/Pat.hs b/compiler/Language/Haskell/Syntax/Pat.hs
index 66b9708bfe..fd5b052433 100644
--- a/compiler/Language/Haskell/Syntax/Pat.hs
+++ b/compiler/Language/Haskell/Syntax/Pat.hs
@@ -22,7 +22,7 @@ module Language.Haskell.Syntax.Pat (
         Pat(..), LPat,
         ConLikeP,
 
-        HsConPatDetails, hsConPatArgs,
+        HsConPatDetails, hsConPatArgs, hsConPatTyArgs,
         HsConPatTyArg(..),
         HsRecFields(..), HsFieldBind(..), LHsFieldBind,
         HsRecField, LHsRecField,
@@ -243,6 +243,11 @@ hsConPatArgs (PrefixCon _ ps) = ps
 hsConPatArgs (RecCon fs)      = Data.List.map (hfbRHS . unXRec @p) (rec_flds fs)
 hsConPatArgs (InfixCon p1 p2) = [p1,p2]
 
+hsConPatTyArgs :: forall p. HsConPatDetails p -> [HsConPatTyArg (NoGhcTc p)]
+hsConPatTyArgs (PrefixCon tyargs _) = tyargs
+hsConPatTyArgs (RecCon _)           = []
+hsConPatTyArgs (InfixCon _ _)       = []
+
 -- | Haskell Record Fields
 --
 -- HsRecFields is used only for patterns and expressions (not data type
diff --git a/testsuite/tests/typecheck/should_compile/T22478.hs b/testsuite/tests/typecheck/should_compile/T22478.hs
new file mode 100644
index 0000000000..d9a10c0457
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T22478.hs
@@ -0,0 +1,72 @@
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE UnboxedSums #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+module T22478 where
+
+import Data.Kind (Type, Constraint)
+import GHC.Exts (Multiplicity(Many))
+import qualified Language.Haskell.TH as TH
+
+data P (a :: k) where
+  MkP :: forall {k} (a :: k). P a
+
+data T (a :: Type) = MkT
+
+fAppTy :: T (Maybe Int) -> (P Maybe, P Int)
+fAppTy (MkT @(f a)) = (MkP @f, MkP @a)
+
+fAppKindTy :: T (P @(Type -> Constraint) Num) -> (P Type, P Constraint, P Num)
+fAppKindTy (MkT @(P @(k1 -> k2) c)) = (MkP @k1, MkP @k2, MkP @c)
+
+fOpTy :: T (Either Int Bool) -> (P Either, P Int, P Bool)
+fOpTy (MkT @(a `op` b)) = (MkP @op, MkP @a, MkP @b)
+
+fQualTy :: T ((Ord a, Num a) => a) -> (P (Ord a), P (Num a), P a)
+fQualTy (MkT @((c1, c2) => a)) = (MkP @c1, MkP @c2, MkP @a)
+
+fFunTy :: T (Int -> Bool) -> (P Int, P Bool, P Many)
+fFunTy (MkT @(a %m -> b)) = (MkP @a, MkP @b, MkP @m)
+
+fListTy :: T [Int] -> P Int
+fListTy (MkT @[a]) = MkP @a
+
+fTupleTy :: T (Int, Bool) -> (P Int, P Bool)
+fTupleTy (MkT @(a, b)) = (MkP @a, MkP @b)
+
+fSumTy :: P (# Int | Bool #) -> (P Int, P Bool)
+fSumTy (MkP @(# a | b #)) = (MkP @a, MkP @b)
+
+fExplicitListTy :: P '[Int, Bool] -> (P Int, P Bool)
+fExplicitListTy (MkP @'[a, b]) = (MkP @a, MkP @b)
+
+fExplicitTupleTy :: P '(Maybe, Functor) -> (P Maybe, P Functor)
+fExplicitTupleTy (MkP @'(m, f)) = (MkP @m, MkP @f)
+
+fKindSig :: P Maybe -> (P Maybe, P (Type -> Type))
+fKindSig (MkP @(t :: k)) = (MkP @t, MkP @k)
+
+-- TODO (int-index):
+--
+-- fForallTy :: T (forall a. a -> b) -> P b
+-- fForallTy (MkT @(forall a. a -> b)) = MkP @b
+
+fIParamTy :: T ((?t :: Type) => Int) -> P Type
+fIParamTy (MkT @((?t :: k) => Int)) = MkP @k
+
+fTyLit :: P "hello" -> ()
+fTyLit (MkP @"hello") = ()
+
+-- TODO (int-index):
+--
+-- fSpliceTy :: T Int -> P Int
+-- fSpliceTy (MkT @($(TH.varT (TH.mkName "t")))) = MkP @t
+--
+--   Error:
+--      • Not in scope: type variable ‘t’
+--      • In the untyped splice: $(TH.varT (TH.mkName "t"))
+--
+--   But should it be an error? I don't think so.
\ No newline at end of file
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 0a1edfa866..52ef780e4b 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -852,3 +852,4 @@ test('T22310', normal, compile, [''])
 test('T22331', normal, compile, [''])
 test('T22516', normal, compile, [''])
 test('T22647', normal, compile, [''])
+test('T22478', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiAppPat.stderr b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiAppPat.stderr
index 87655cb6cf..91866377fb 100644
--- a/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiAppPat.stderr
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiAppPat.stderr
@@ -1,4 +1,6 @@
 
-TyAppPat_NonlinearMultiAppPat.hs:13:6: error:
-    Type variable ‘a’ is already in scope.
-    Type applications in patterns must bind fresh variables, without shadowing.
+TyAppPat_NonlinearMultiAppPat.hs:13:13: error:
+    • Conflicting definitions for ‘a’
+      Bound at: TyAppPat_NonlinearMultiAppPat.hs:13:13
+                TyAppPat_NonlinearMultiAppPat.hs:13:16
+    • In an equation for ‘foo’
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiPat.stderr b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiPat.stderr
index 82c78654f7..f1ff2df9a6 100644
--- a/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiPat.stderr
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiPat.stderr
@@ -1,16 +1,24 @@
 
-TyAppPat_NonlinearMultiPat.hs:10:19: error:
-    Type variable ‘a’ is already in scope.
-    Type applications in patterns must bind fresh variables, without shadowing.
+TyAppPat_NonlinearMultiPat.hs:10:15: error:
+    • Conflicting definitions for ‘a’
+      Bound at: TyAppPat_NonlinearMultiPat.hs:10:15
+                TyAppPat_NonlinearMultiPat.hs:10:28
+    • In an equation for ‘foo’
 
-TyAppPat_NonlinearMultiPat.hs:11:18: error:
-    Type variable ‘a’ is already in scope.
-    Type applications in patterns must bind fresh variables, without shadowing.
+TyAppPat_NonlinearMultiPat.hs:11:12: error:
+    • Conflicting definitions for ‘a’
+      Bound at: TyAppPat_NonlinearMultiPat.hs:11:12
+                TyAppPat_NonlinearMultiPat.hs:11:27
+    • In an equation for ‘foo’
 
-TyAppPat_NonlinearMultiPat.hs:12:19: error:
-    Type variable ‘a’ is already in scope.
-    Type applications in patterns must bind fresh variables, without shadowing.
+TyAppPat_NonlinearMultiPat.hs:12:15: error:
+    • Conflicting definitions for ‘a’
+      Bound at: TyAppPat_NonlinearMultiPat.hs:12:15
+                TyAppPat_NonlinearMultiPat.hs:12:25
+    • In an equation for ‘foo’
 
-TyAppPat_NonlinearMultiPat.hs:13:18: error:
-    Type variable ‘a’ is already in scope.
-    Type applications in patterns must bind fresh variables, without shadowing.
+TyAppPat_NonlinearMultiPat.hs:13:12: error:
+    • Conflicting definitions for ‘a’
+      Bound at: TyAppPat_NonlinearMultiPat.hs:13:12
+                TyAppPat_NonlinearMultiPat.hs:13:24
+    • In an equation for ‘foo’
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearSinglePat.stderr b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearSinglePat.stderr
index 0d06da09d2..6265feda89 100644
--- a/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearSinglePat.stderr
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearSinglePat.stderr
@@ -1,3 +1,6 @@
 
-TyAppPat_NonlinearSinglePat.hs:13:6: error:
-    Variable `a' would be bound multiple times by a type argument.
+TyAppPat_NonlinearSinglePat.hs:13:14: error:
+    • Conflicting definitions for ‘a’
+      Bound at: TyAppPat_NonlinearSinglePat.hs:13:14
+                TyAppPat_NonlinearSinglePat.hs:13:16
+    • In an equation for ‘foo’