type checker checkpointwip/17594-another-approach-typecheck

36 files changed, 307 insertions, 240 deletions

diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 166a56cabb..f320f2d95a 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -49,7 +49,7 @@ module GHC.Core.Type (
         mkSpecForAllTy, mkSpecForAllTys,
         mkVisForAllTys, mkTyCoInvForAllTy,
         mkInfForAllTy, mkInfForAllTys,
-        splitForAllTyCoVars,
+        splitForAllTyVars, splitForAllTyCoVars,
         splitForAllReqTVBinders, splitForAllInvisTVBinders,
         splitForAllTyCoVarBinders,
         splitForAllTyCoVar_maybe, splitForAllTyCoVar,
@@ -100,8 +100,8 @@ module GHC.Core.Type (
         mkAnonBinder,
         isAnonTyCoBinder,
         binderVar, binderVars, binderType, binderArgFlag,
-        tyCoBinderType, tyCoBinderVar_maybe,
-        tyBinderType,
+        tyCoBinderType, tyCoBinderMult, tyCoBinderScaledType, tyCoBinderVar_maybe,
+        tyBinderType, toAnonTyCoBinder,
         binderRelevantType_maybe,
         isVisibleArgFlag, isInvisibleArgFlag, isVisibleBinder,
         isInvisibleBinder, isNamedBinder,
@@ -2365,6 +2365,16 @@ tyCoBinderType :: TyCoBinder -> Type
 tyCoBinderType (Named tvb) = binderType tvb
 tyCoBinderType (Anon _ ty)   = scaledThing ty
 
+tyCoBinderMult :: TyCoBinder -> Mult
+tyCoBinderMult (Anon _ ty) = scaledMult ty
+tyCoBinderMult _           = Many
+
+tyCoBinderScaledType :: TyCoBinder -> Scaled Type
+tyCoBinderScaledType bndr = Scaled (tyCoBinderMult bndr) (tyCoBinderType bndr)
+
+toAnonTyCoBinder :: Scaled Type -> TyCoBinder
+toAnonTyCoBinder scaled_ty = Anon VisArg scaled_ty
+
 tyBinderType :: TyBinder -> Type
 tyBinderType (Named (Bndr tv _))
   = assert (isTyVar tv )
diff --git a/compiler/GHC/Hs/Expr.hs b/compiler/GHC/Hs/Expr.hs
index d27cf835d5..918026fda8 100644
--- a/compiler/GHC/Hs/Expr.hs
+++ b/compiler/GHC/Hs/Expr.hs
@@ -67,6 +67,8 @@ import {-# SOURCE #-} GHC.Tc.Types (TcLclEnv)
 import GHCi.RemoteTypes ( ForeignRef )
 import qualified Language.Haskell.TH as TH (Q)
 
+import Language.Haskell.Syntax.Pat (isInvis)
+
 -- libraries:
 import Data.Data hiding (Fixity(..))
 import qualified Data.Data as Data (Fixity(..))
@@ -1286,7 +1288,7 @@ type instance XMG         GhcTc b = MatchGroupTc
 
 data MatchGroupTc
   = MatchGroupTc
-       { mg_arg_tys :: [Scaled Type]  -- Types of the arguments, t1..tn
+       { mg_arg_tys :: [TyCoBinder]  -- Types of the arguments, t1..tn
        , mg_res_ty  :: Type    -- Type of the result, tr
        , mg_origin  :: Origin  -- Origin (Generated vs FromSource)
        } deriving Data
@@ -1319,9 +1321,16 @@ matchGroupArity (MG { mg_alts = alts })
   | L _ (alt1:_) <- alts = length (hsLMatchPats alt1)
   | otherwise        = panic "matchGroupArity"
 
+matchGroupLMatchPats :: MatchGroup (GhcPass id) body -> [LMatchPat (GhcPass id)]
+matchGroupLMatchPats (MG { mg_alts = (L _ (alt : _)) }) = hsLMatchPats alt
+matchGroupLMatchPats _ = panic "matchGroupLMatchPats"
+
 hsLMatchPats :: LMatch (GhcPass id) body -> [LMatchPat (GhcPass id)]
 hsLMatchPats (L _ (Match { m_pats = pats })) = pats
 
+hasInvisPats :: MatchGroup (GhcPass id) body -> Bool
+hasInvisPats mg = any isInvis (matchGroupLMatchPats mg)
+
 -- We keep the type checker happy by providing EpAnnComments.  They
 -- can only be used if they follow a `where` keyword with no binds,
 -- but in that case the comment is attached to the following parsed
diff --git a/compiler/GHC/Hs/Pat.hs b/compiler/GHC/Hs/Pat.hs
index a88d2ed398..e5d12d6f46 100644
--- a/compiler/GHC/Hs/Pat.hs
+++ b/compiler/GHC/Hs/Pat.hs
@@ -39,7 +39,7 @@ module GHC.Hs.Pat (
 
         mkPrefixConPat, mkCharLitPat, mkNilPat, mkVisPat, expectVisPats,
 
-        isSimplePat,
+        isSimplePat, isSimpleMatchPat,
         looksLazyPatBind,
         isBangedLPat,
         gParPat, patNeedsParens, parenthesizePat, parenthesizeLMatchPat,
@@ -175,13 +175,11 @@ type instance XHsFieldBind _ = EpAnn [AddEpAnn]
 
 type instance XVisPat (GhcPass _) = NoExtField
 
-type instance XInvisTyVarPat GhcPs = NoExtField
-type instance XInvisTyVarPat GhcRn = NoExtField
-type instance XInvisTyVarPat GhcTc = DataConCantHappen
+type instance XInvisTyVarPat (GhcPass _) = NoExtField
 
 type instance XInvisWildTyPat GhcPs = NoExtField
 type instance XInvisWildTyPat GhcRn = NoExtField
-type instance XInvisWildTyPat GhcTc = DataConCantHappen
+type instance XInvisWildTyPat GhcTc = Type
 
 type instance XXMatchPat (GhcPass _) = DataConCantHappen
 
@@ -193,9 +191,8 @@ expectVisPats :: [LMatchPat GhcTc] -> [LPat GhcTc]
 expectVisPats xs = map toLPat xs
   where
     toLPat :: LMatchPat GhcTc -> LPat GhcTc
-    toLPat (L _ (VisPat _ pat))      = pat
-    toLPat (L _ (InvisTyVarPat x _)) = dataConCantHappen x
-    toLPat (L _ (InvisWildTyPat x))  = dataConCantHappen x
+    toLPat (L _ (VisPat _ pat)) = pat
+    toLPat _                    = panic "at the moment, @-binders are not allowed yet"
 
 -- ---------------------------------------------------------------------
 
@@ -232,6 +229,7 @@ data XXPatGhcTc
   -- See Note [Rebindable syntax and HsExpansion].
   | ExpansionPat (Pat GhcRn) (Pat GhcTc)
 
+
 -- See Note [Rebindable syntax and HsExpansion].
 data HsPatExpansion a b
   = HsPatExpanded a b
@@ -319,9 +317,6 @@ instance OutputableBndrId p => Outputable (MatchPat (GhcPass p)) where
 pprLPat :: (OutputableBndrId p) => LPat (GhcPass p) -> SDoc
 pprLPat (L _ e) = pprPat e
 
-pprLMatchPat :: (OutputableBndrId p) => LMatchPat (GhcPass p) -> SDoc
-pprLMatchPat (L _ e) = ppr e
-
 -- | Print with type info if -dppr-debug is on
 pprPatBndr :: OutputableBndr name => name -> SDoc
 pprPatBndr var
@@ -654,6 +649,11 @@ isSimplePat p = case unLoc p of
   VarPat _ x -> Just (unLoc x)
   _ -> Nothing
 
+isSimpleMatchPat :: LMatchPat (GhcPass x) -> Maybe (IdP (GhcPass x))
+isSimpleMatchPat p = case unLoc p of
+  VisPat _ lpat -> isSimplePat lpat
+  InvisTyVarPat _ bndr -> Just (hsLTyVarName bndr)
+  _ -> Nothing
 
 {- Note [Unboxed sum patterns aren't irrefutable]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/GHC/Hs/Pat.hs-boot b/compiler/GHC/Hs/Pat.hs-boot
index 4056823581..c3cfbdf993 100644
--- a/compiler/GHC/Hs/Pat.hs-boot
+++ b/compiler/GHC/Hs/Pat.hs-boot
@@ -16,4 +16,3 @@ instance (OutputableBndrId p) => Outputable (Pat (GhcPass p))
 instance (OutputableBndrId p) => Outputable (MatchPat (GhcPass p))
 
 pprLPat :: (OutputableBndrId p) => LPat (GhcPass p) -> SDoc
-pprLMatchPat :: (OutputableBndrId p) => LMatchPat (GhcPass p) -> SDoc
diff --git a/compiler/GHC/Hs/Syn/Type.hs b/compiler/GHC/Hs/Syn/Type.hs
index 073b45cfeb..af0810e9a6 100644
--- a/compiler/GHC/Hs/Syn/Type.hs
+++ b/compiler/GHC/Hs/Syn/Type.hs
@@ -43,8 +43,9 @@ hsLPatType :: LPat GhcTc -> Type
 hsLPatType (L _ p) = hsPatType p
 
 hsLMatchPatType :: LMatchPat GhcTc -> Type
-hsLMatchPatType (L _ (VisPat _ p)) = hsPatType (unLoc p)
-hsLMatchPatType _                  = panic "@-binders in functions are not allowed yet"
+hsLMatchPatType (L _ (VisPat _ p))           = hsPatType (unLoc p)
+hsLMatchPatType (L _ (InvisTyVarPat _ bndr)) = hsTyVarBndrTy (unLoc bndr)
+hsLMatchPatType (L _ (InvisWildTyPat ty))    = ty
 
 hsPatType :: Pat GhcTc -> Type
 hsPatType (ParPat _ _ pat _)            = hsLPatType pat
@@ -198,7 +199,7 @@ lhsCmdTopType :: LHsCmdTop GhcTc -> Type
 lhsCmdTopType (L _ (HsCmdTop (CmdTopTc _ ret_ty _) _)) = ret_ty
 
 matchGroupTcType :: MatchGroupTc -> Type
-matchGroupTcType (MatchGroupTc args res _) = mkVisFunTys args res
+matchGroupTcType (MatchGroupTc args res _) = mkPiTys args res
 
 syntaxExprType :: SyntaxExpr GhcTc -> Type
 syntaxExprType (SyntaxExprTc e _ _) = hsExprType e
diff --git a/compiler/GHC/Hs/Type.hs b/compiler/GHC/Hs/Type.hs
index 61df0cb15a..da367cb84e 100644
--- a/compiler/GHC/Hs/Type.hs
+++ b/compiler/GHC/Hs/Type.hs
@@ -79,7 +79,7 @@ module GHC.Hs.Type (
         mkHsOpTy, mkHsAppTy, mkHsAppTys, mkHsAppKindTy,
         ignoreParens, hsSigWcType, hsPatSigType,
         hsTyKindSig,
-        setHsTyVarBndrFlag, hsTyVarBndrFlag, hsTyVarBndrId,
+        setHsTyVarBndrFlag, hsTyVarBndrFlag, hsTyVarBndrTy,
 
         -- Printing
         pprHsType, pprHsForAll,
@@ -100,7 +100,7 @@ import GHC.Hs.Extension
 import GHC.Parser.Annotation
 
 import GHC.Types.Fixity ( LexicalFixity(..) )
-import GHC.Types.Id ( Id )
+import GHC.Types.Id ( Id, idType )
 import GHC.Types.SourceText
 import GHC.Types.Name( Name, NamedThing(getName) )
 import GHC.Types.Name.Reader ( RdrName )
@@ -115,7 +115,6 @@ import GHC.Types.Basic
 import GHC.Types.SrcLoc
 import GHC.Utils.Outputable
 import GHC.Utils.Misc (count)
-import GHC.Utils.Panic (panic)
 
 import Data.Maybe
 import Data.Data (Data)
@@ -285,11 +284,9 @@ hsTyVarBndrFlag :: HsTyVarBndr flag (GhcPass pass) -> flag
 hsTyVarBndrFlag (UserTyVar _ fl _)     = fl
 hsTyVarBndrFlag (KindedTyVar _ fl _ _) = fl
 
--- | Return the attached lidp
-hsTyVarBndrId :: HsTyVarBndr flag pass -> LIdP pass
-hsTyVarBndrId (UserTyVar _ _ lipd)     = lipd
-hsTyVarBndrId (KindedTyVar _ _ lipd _) = lipd
-hsTyVarBndrId _                        = panic "hsTyVarBndrId: no LIdP"
+hsTyVarBndrTy :: HsTyVarBndr flag GhcTc -> Type
+hsTyVarBndrTy (UserTyVar _ _ lipd)     = idType (unLoc lipd)
+hsTyVarBndrTy (KindedTyVar _ _ lipd _) = idType (unLoc lipd)
 
 -- | Set the attached flag
 setHsTyVarBndrFlag :: flag -> HsTyVarBndr flag' (GhcPass pass)
diff --git a/compiler/GHC/HsToCore/Arrows.hs b/compiler/GHC/HsToCore/Arrows.hs
index 9b326043fe..ccf459ae04 100644
--- a/compiler/GHC/HsToCore/Arrows.hs
+++ b/compiler/GHC/HsToCore/Arrows.hs
@@ -38,11 +38,13 @@ import GHC.Core
 import GHC.Core.FVs
 import GHC.Core.Utils
 import GHC.Core.Make
+import GHC.Core.Type (tyCoBinderScaledType)
 import GHC.HsToCore.Binds (dsHsWrapper)
 
 
 import GHC.Types.Id
 import GHC.Core.ConLike
+import GHC.Core.TyCo.Rep (TyCoBinder(..))
 import GHC.Builtin.Types
 import GHC.Types.Basic
 import GHC.Builtin.Names
@@ -531,7 +533,7 @@ multiple scrutinees)
 dsCmd ids local_vars stack_ty res_ty
       (HsCmdLamCase _ lc_variant match@MG { mg_ext = MatchGroupTc {mg_arg_tys = arg_tys} } )
       env_ids = do
-    arg_ids <- newSysLocalsDs arg_tys
+    arg_ids <- newSysLocalsDs (map tyCoBinderScaledType arg_tys)
 
     let match_ctxt = ArrowLamCaseAlt lc_variant
         pat_vars = mkVarSet arg_ids
@@ -805,7 +807,7 @@ dsCases ids local_vars stack_id stack_ty res_ty
     Nothing -> ([], void_ty,) . do_arr ids void_ty res_ty <$>
       dsExpr (HsLamCase EpAnnNotUsed LamCase
         (MG { mg_alts = noLocA []
-            , mg_ext = MatchGroupTc [Scaled Many void_ty] res_ty Generated
+            , mg_ext = MatchGroupTc [Anon VisArg (Scaled Many void_ty)] res_ty Generated
             }))
 
       -- Replace the commands in the case with these tagged tuples,
diff --git a/compiler/GHC/HsToCore/Expr.hs b/compiler/GHC/HsToCore/Expr.hs
index 90c786e98a..f41c31f082 100644
--- a/compiler/GHC/HsToCore/Expr.hs
+++ b/compiler/GHC/HsToCore/Expr.hs
@@ -1,4 +1,5 @@
 
+
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE ViewPatterns #-}
 
@@ -759,7 +760,7 @@ dsDo ctx stmts
                            (MG { mg_alts = noLocA [mkSimpleMatch
                                                     LambdaExpr
                                                     [mkVisPat mfix_pat] body]
-                               , mg_ext = MatchGroupTc [unrestricted tup_ty] body_ty Generated
+                               , mg_ext = MatchGroupTc [Anon VisArg (unrestricted tup_ty)] body_ty Generated
                                })
         mfix_pat     = noLocA $ LazyPat noExtField $ mkBigLHsPatTupId rec_tup_pats
         body         = noLocA $ HsDo body_ty
diff --git a/compiler/GHC/HsToCore/Match.hs b/compiler/GHC/HsToCore/Match.hs
index 57490dea2b..3e783d97fa 100644
--- a/compiler/GHC/HsToCore/Match.hs
+++ b/compiler/GHC/HsToCore/Match.hs
@@ -770,11 +770,11 @@ matchWrapper ctxt scrs (MG { mg_alts = L _ matches
         ; locn   <- getSrcSpanDs
 
         ; new_vars    <- case matches of
-                           []    -> newSysLocalsDs arg_tys
+                           []    -> newSysLocalsDs' arg_tys
                            (m:_) ->
                             selectMatchVars (zipWithEqual "matchWrapper"
                                               (\a b -> (scaledMult a, unLoc b))
-                                                arg_tys
+                                                (map tyCoBinderScaledType arg_tys)
                                                 (expectVisPats (hsLMatchPats m)))
 
         -- Pattern match check warnings for /this match-group/.
diff --git a/compiler/GHC/HsToCore/Monad.hs b/compiler/GHC/HsToCore/Monad.hs
index 9211b52fd7..7569dcb701 100644
--- a/compiler/GHC/HsToCore/Monad.hs
+++ b/compiler/GHC/HsToCore/Monad.hs
@@ -20,7 +20,7 @@ module GHC.HsToCore.Monad (
         Applicative(..),(<$>),
 
         duplicateLocalDs, newSysLocalDs,
-        newSysLocalsDs, newUniqueId,
+        newSysLocalsDs, newSysLocalsDs', newUniqueId,
         newFailLocalDs, newPredVarDs,
         getSrcSpanDs, putSrcSpanDs, putSrcSpanDsA,
         mkPrintUnqualifiedDs,
@@ -73,6 +73,7 @@ import GHC.Core.ConLike
 import GHC.Core.TyCon
 import GHC.Core.Type
 import GHC.Core.Multiplicity
+import GHC.Core.TyCo.Rep ( TyCoBinder(..) )
 
 import GHC.IfaceToCore
 
@@ -101,6 +102,7 @@ import GHC.Types.Literal ( mkLitString )
 import GHC.Types.CostCentre.State
 import GHC.Types.TyThing
 import GHC.Types.Error
+import GHC.Types.Var
 
 import GHC.Utils.Error
 import GHC.Utils.Outputable
@@ -387,6 +389,12 @@ newFailLocalDs = mkSysLocalM (fsLit "fail")
 newSysLocalsDs :: [Scaled Type] -> DsM [Id]
 newSysLocalsDs = mapM (\(Scaled w t) -> newSysLocalDs w t)
 
+newSysLocalsDs' :: [TyCoBinder] -> DsM [Id]
+newSysLocalsDs' = mapM newSysLocTyCoBinder where
+  newSysLocTyCoBinder (Anon _ (Scaled w t)) = newSysLocalDs w t
+  newSysLocTyCoBinder (Named (Bndr tv _))   = newSysLocalDs Many (varType tv)
+
+
 {-
 We can also reach out and either set/grab location information from
 the @SrcSpan@ being carried around.
diff --git a/compiler/GHC/HsToCore/Pmc/Desugar.hs b/compiler/GHC/HsToCore/Pmc/Desugar.hs
index 272021b6c9..3b3ace347c 100644
--- a/compiler/GHC/HsToCore/Pmc/Desugar.hs
+++ b/compiler/GHC/HsToCore/Pmc/Desugar.hs
@@ -257,8 +257,7 @@ desugarLPat x = desugarPat x . unLoc
 -- | Desugar a match pattern
 desugarLMatchPat :: Id -> LMatchPat GhcTc -> DsM [PmGrd]
 desugarLMatchPat x (L _ (VisPat _ pat))      = desugarLPat x pat
-desugarLMatchPat _ (L _ (InvisTyVarPat x _)) = dataConCantHappen x
-desugarLMatchPat _ (L _ (InvisWildTyPat x))  = dataConCantHappen x
+desugarLMatchPat _ _                         = panic "desugarLMatchPat"
 
 -- | 'desugarLPat', but also select and return a new match var.
 desugarLPatV :: LPat GhcTc -> DsM (Id, [PmGrd])
diff --git a/compiler/GHC/Parser.y b/compiler/GHC/Parser.y
index 805135f239..a226ae4531 100644
--- a/compiler/GHC/Parser.y
+++ b/compiler/GHC/Parser.y
@@ -3326,9 +3326,9 @@ matchpats :: { [LMatchPat GhcPs] }
 apat   :: { LPat GhcPs }
 apat    : aexp                  {% (checkPattern <=< runPV) (unECP $1) }
 
-apats :: { [LMatchPat GhcPs] }
-       : matchpat matchpats            { $1 : $2 }
-           | {- empty -}                   { [] }
+apats :: { [LPat GhcPs] }
+       : apat apats            { $1 : $2 }
+       | {- empty -}           { [] }
 
 -----------------------------------------------------------------------------
 -- Statement sequences
diff --git a/compiler/GHC/Parser/PostProcess.hs b/compiler/GHC/Parser/PostProcess.hs
index cccf1910b7..be71b56ae6 100644
--- a/compiler/GHC/Parser/PostProcess.hs
+++ b/compiler/GHC/Parser/PostProcess.hs
@@ -61,8 +61,6 @@ module GHC.Parser.PostProcess (
         checkPrecP,           -- Int -> P Int
         checkContext,         -- HsType -> P HsContext
         checkPattern,         -- HsExp -> P HsPat
-        checkLMatchPattern,
-        mkInvisPatBuilder,
         checkPattern_details,
         incompleteDoBlock,
         ParseContext(..),
@@ -1330,7 +1328,7 @@ checkPatBind loc annsIn (L _ (BangPat (EpAnn _ ans cs) (L _ (VarPat _ v))))
                                     , mc_fixity = Prefix
                                     , mc_strictness = SrcStrict }
                   , m_pats = []
-                  , m_grhss = grhss }
+                 , m_grhss = grhss }
 
 checkPatBind loc annsIn lhs (L _ grhss) = do
   cs <- getCommentsFor loc
@@ -1385,7 +1383,6 @@ isFunLhs e = go e [] [] []
      where
        (o,c) = mkParensEpAnn (realSrcSpan $ locA l)
    go (L loc (PatBuilderOpApp l (L loc' op) r (EpAnn loca anns cs))) es ops cps
-<<<<<<< HEAD
       | not (isRdrDataCon op)         -- We have found the function!
       = return (Just (L loc' op, Infix, (mk l:mk r:es), (anns ++ reverse ops ++ cps)))
       | otherwise                     -- Infix data con; keep going
@@ -1401,35 +1398,6 @@ isFunLhs e = go e [] [] []
    go (L _ (PatBuilderAppType pat _ (HsPS _ (L loc hs_ty)))) es ops cps
              | Just arg <- go_type_arg hs_ty
              = go pat (L loc (MatchPatBuilderMatchPat arg) : es) ops cps
-||||||| parent of cf7104c386 (parser and renamer checkpoint)
-        | not (isRdrDataCon op)         -- We have found the function!
-        = return (Just (L loc' op, Infix, (l:r:es), (anns ++ reverse ops ++ cps)))
-        | otherwise                     -- Infix data con; keep going
-        = do { mb_l <- go l es ops cps
-             ; case mb_l of
-                 Just (op', Infix, j : k : es', anns')
-                   -> return (Just (op', Infix, j : op_app : es', anns'))
-                   where
-                     op_app = L loc (PatBuilderOpApp k
-                               (L loc' op) r (EpAnn loca (reverse ops++cps) cs))
-                 _ -> return Nothing }
-=======
-      | not (isRdrDataCon op)         -- We have found the function!
-      = return (Just (L loc' op, Infix, (mk l:mk r:es), (anns ++ reverse ops ++ cps)))
-      | otherwise                     -- Infix data con; keep going
-      = do { mb_l <- go l es ops cps
-           ; return (join $ fmap reassociate mb_l) }
-        where
-          reassociate (op', Infix, j : L k_loc (MatchPatBuilderVisPat k) : es', anns')
-            = Just (op', Infix, j : op_app : es', anns')
-            where
-              op_app = mk $ L loc (PatBuilderOpApp (L k_loc k) (L loc' op) r
-                                    (EpAnn loca (reverse ops ++ cps) cs))
-          reassociate _other = Nothing
-   go (L _ (PatBuilderAppType pat (HsPS _ (L loc hs_ty)))) es ops cps
-             | Just arg <- go_type_arg hs_ty
-             = go pat (L loc (MatchPatBuilderMatchPat arg) : es) ops cps
->>>>>>> cf7104c386 (parser and renamer checkpoint)
    go _ _ _ _ = return Nothing
 
    go_type_arg :: HsType GhcPs -> Maybe (MatchPat GhcPs)
diff --git a/compiler/GHC/Parser/Types.hs b/compiler/GHC/Parser/Types.hs
index 53cb3d93fc..a89472cc5f 100644
--- a/compiler/GHC/Parser/Types.hs
+++ b/compiler/GHC/Parser/Types.hs
@@ -54,7 +54,6 @@ pprSumOrTuple boxity = \case
 -- | See Note [Ambiguous syntactic categories] and Note [PatBuilder]
 data PatBuilder p
   = PatBuilderPat (Pat p)
-  | PatBuilderMatchPat (MatchPat p)
   | PatBuilderPar (LHsToken "(" p) (LocatedA (PatBuilder p)) (LHsToken ")" p)
   | PatBuilderApp (LocatedA (PatBuilder p)) (LocatedA (PatBuilder p))
   | PatBuilderAppType (LocatedA (PatBuilder p)) (LHsToken "@" p) (HsPatSigType GhcPs)
@@ -69,7 +68,6 @@ data MatchPatBuilder p
 
 instance Outputable (PatBuilder GhcPs) where
   ppr (PatBuilderPat p) = ppr p
-  ppr (PatBuilderMatchPat p) = ppr p
   ppr (PatBuilderPar _ (L _ p) _) = parens (ppr p)
   ppr (PatBuilderApp (L _ p1) (L _ p2)) = ppr p1 <+> ppr p2
   ppr (PatBuilderAppType (L _ p) _ t) = ppr p <+> text "@" <> ppr t
diff --git a/compiler/GHC/Tc/Deriv/Generics.hs b/compiler/GHC/Tc/Deriv/Generics.hs
index 3a024bf3b4..bae4ca79bf 100644
--- a/compiler/GHC/Tc/Deriv/Generics.hs
+++ b/compiler/GHC/Tc/Deriv/Generics.hs
@@ -363,7 +363,7 @@ mkBindsRep dflags gk loc dit@(DerivInstTys{dit_rep_tc = tycon}) = (binds, sigs)
         -- to save some allocations during typechecking.
         -- See Note [Generics compilation speed tricks]
         from_eqn = mkHsCaseAlt x_Pat $ mkM1_E
-                                     $ nlHsPar $ nlHsCase x_Expr from_matches
+                                       $ nlHsPar $ nlHsCase x_Expr from_matches
         to_eqn   = mkHsCaseAlt (mkM1_P x_Pat) $ nlHsCase x_Expr to_matches
 
         from_matches  = [mkHsCaseAlt pat rhs | (pat,rhs) <- from_alts]
diff --git a/compiler/GHC/Tc/Gen/Arrow.hs b/compiler/GHC/Tc/Gen/Arrow.hs
index 90759851f9..95e5c8e7c1 100644
--- a/compiler/GHC/Tc/Gen/Arrow.hs
+++ b/compiler/GHC/Tc/Gen/Arrow.hs
@@ -18,6 +18,7 @@ import GHC.Prelude
 import {-# SOURCE #-}   GHC.Tc.Gen.Expr( tcCheckMonoExpr, tcInferRho, tcSyntaxOp
                                        , tcCheckPolyExpr )
 
+import GHC.Core.Type ( toAnonTyCoBinder )
 import GHC.Hs
 import GHC.Tc.Errors.Types
 import GHC.Tc.Gen.Match
@@ -343,13 +344,13 @@ tcCmdMatchLambda env
                  (cmd_stk, res_ty)
   = do { (co, arg_tys, cmd_stk') <- matchExpectedCmdArgs n_pats cmd_stk
 
-       ; let check_arg_tys = map (unrestricted . mkCheckExpType) arg_tys
+       ; let check_arg_tys = map (\ty -> ExpAnon VisArg ((unrestricted . mkCheckExpType) ty)) arg_tys
        ; matches' <- forM matches $
            addErrCtxt . pprMatchInCtxt . unLoc <*> tc_match check_arg_tys cmd_stk'
 
        ; let arg_tys' = map unrestricted arg_tys
              mg' = mg { mg_alts = L l matches'
-                      , mg_ext = MatchGroupTc arg_tys' res_ty origin }
+                      , mg_ext = MatchGroupTc (map toAnonTyCoBinder arg_tys') res_ty origin }
 
        ; return (mkWpCastN co, mg') }
   where
diff --git a/compiler/GHC/Tc/Gen/Bind.hs b/compiler/GHC/Tc/Gen/Bind.hs
index 21d1424317..6130f76c2c 100644
--- a/compiler/GHC/Tc/Gen/Bind.hs
+++ b/compiler/GHC/Tc/Gen/Bind.hs
@@ -610,13 +610,14 @@ tcPolyCheck prag_fn
                 -- See Note [Instantiate sig with fresh variables]
 
                 let mono_id = mkLocalId mono_name (varMult poly_id) rho_ty in
+                let ty = if hasInvisPats matches then (idType poly_id) else rho_ty in
                 tcExtendBinderStack [TcIdBndr mono_id NotTopLevel] $
                 -- Why mono_id in the BinderStack?
                 --    See Note [Relevant bindings and the binder stack]
 
                 setSrcSpanA bind_loc $
                 tcMatchesFun (L nm_loc mono_id) matches
-                             (mkCheckExpType rho_ty)
+                             (mkCheckExpType ty)
 
        -- We make a funny AbsBinds, abstracting over nothing,
        -- just so we have somewhere to put the SpecPrags.
diff --git a/compiler/GHC/Tc/Gen/Expr.hs b/compiler/GHC/Tc/Gen/Expr.hs
index 92d7709089..e71f165322 100644
--- a/compiler/GHC/Tc/Gen/Expr.hs
+++ b/compiler/GHC/Tc/Gen/Expr.hs
@@ -754,9 +754,9 @@ tcSynArgE orig op sigma_ty syn_ty thing_inside
              , ( ( (result, arg_ty, res_ty, op_mult)
                  , res_wrapper )                     -- :: res_ty_out "->" res_ty
                , arg_wrapper1, [], arg_wrapper2 ) )  -- :: arg_ty "->" arg_ty_out
-               <- matchExpectedFunTys herald GenSigCtxt 1 (mkCheckExpType rho_ty) $
+               <- matchExpectedFunTys herald GenSigCtxt match_group (mkCheckExpType rho_ty) $
                   \ [arg_ty] res_ty ->
-                  do { arg_tc_ty <- expTypeToType (scaledThing arg_ty)
+                  do { arg_tc_ty <- expTypeToType (expTyBinderType arg_ty)
                      ; res_tc_ty <- expTypeToType res_ty
 
                          -- another nested arrow is too much for now,
@@ -767,7 +767,7 @@ tcSynArgE orig op sigma_ty syn_ty thing_inside
                                   (text "Too many nested arrows in SyntaxOpType" $$
                                    pprCtOrigin orig)
 
-                     ; let arg_mult = scaledMult arg_ty
+                     ; let arg_mult = expTyBinderMult arg_ty
                      ; tcSynArgA orig op arg_tc_ty [] arg_shape $
                        \ arg_results arg_res_mults ->
                        tcSynArgE orig op res_tc_ty res_shape $
@@ -782,6 +782,8 @@ tcSynArgE orig op sigma_ty syn_ty thing_inside
            ; return (result, match_wrapper <.> fun_wrap) }
       where
         herald = ExpectedFunTySyntaxOp orig op
+        match = mkMatch LambdaExpr [mkVisPat (L noSrcSpanA (WildPat noExtField))] (L noSrcSpanA op) emptyLocalBinds
+        match_group = mkMatchGroup Generated (L noSrcSpanA [match])
 
     go rho_ty (SynType the_ty)
       = do { wrap   <- tcSubTypePat orig GenSigCtxt the_ty rho_ty
diff --git a/compiler/GHC/Tc/Gen/Match.hs b/compiler/GHC/Tc/Gen/Match.hs
index 778e6f0365..cbac27896d 100644
--- a/compiler/GHC/Tc/Gen/Match.hs
+++ b/compiler/GHC/Tc/Gen/Match.hs
@@ -42,6 +42,7 @@ import {-# SOURCE #-}   GHC.Tc.Gen.Expr( tcSyntaxOp, tcInferRho, tcInferRhoNC
                                        , tcCheckMonoExpr, tcCheckMonoExprNC
                                        , tcCheckPolyExpr )
 
+import GHC.Types.Basic ( Origin(..) )
 import GHC.Tc.Errors.Types
 import GHC.Tc.Utils.Monad
 import GHC.Tc.Utils.Env
@@ -95,7 +96,7 @@ same number of arguments before using @tcMatches@ to do the work.
 
 tcMatchesFun :: LocatedN Id -- MatchContext Id
              -> MatchGroup GhcRn (LHsExpr GhcRn)
-             -> ExpRhoType    -- Expected type of function
+             -> ExpSigmaType      -- Expected type of function
              -> TcM (HsWrapper, MatchGroup GhcTc (LHsExpr GhcTc))
                                 -- Returns type of body
 tcMatchesFun fun_id matches exp_ty
@@ -110,7 +111,7 @@ tcMatchesFun fun_id matches exp_ty
            -- unfilled thunk
         ; checkArgCounts fun_name matches
 
-        ; matchExpectedFunTys herald ctxt arity exp_ty $ \ pat_tys rhs_ty ->
+        ; matchExpectedFunTys herald ctxt matches exp_ty $ \ bndrs rhs_ty ->
              -- NB: exp_type may be polymorphic, but
              --     matchExpectedFunTys can cope with that
           tcScalingUsage Many $
@@ -120,10 +121,9 @@ tcMatchesFun fun_id matches exp_ty
           -- being scaled by Many. When let binders come with a
           -- multiplicity, then @tcMatchesFun@ will have to take
           -- a multiplicity argument, and scale accordingly.
-          tcMatches match_ctxt pat_tys rhs_ty matches }
+          tcMatches match_ctxt bndrs rhs_ty matches }
   where
     fun_name = idName (unLoc fun_id)
-    arity  = matchGroupArity matches
     herald = ExpectedFunTyMatches (NameThing fun_name) matches
     ctxt   = GenSigCtxt  -- Was: FunSigCtxt fun_name True
                          -- But that's wrong for f :: Int -> forall a. blah
@@ -156,7 +156,7 @@ tcMatchesCase :: (AnnoBody body) =>
                 -- wrapper goes from MatchGroup's ty to expected ty
 
 tcMatchesCase ctxt (Scaled scrut_mult scrut_ty) matches res_ty
-  = tcMatches ctxt [Scaled scrut_mult (mkCheckExpType scrut_ty)] res_ty matches
+  = tcMatches ctxt [ExpAnon VisArg (Scaled scrut_mult (mkCheckExpType scrut_ty))] res_ty matches
 
 tcMatchLambda :: ExpectedFunTyOrigin -- see Note [Herald for matchExpectedFunTys] in GHC.Tc.Utils.Unify
               -> TcMatchCtxt HsExpr
@@ -165,12 +165,15 @@ tcMatchLambda :: ExpectedFunTyOrigin -- see Note [Herald for matchExpectedFunTys
               -> TcM (HsWrapper, MatchGroup GhcTc (LHsExpr GhcTc))
 tcMatchLambda herald match_ctxt match res_ty
   =  do { checkPatCounts (mc_what match_ctxt) match
-        ; matchExpectedFunTys herald GenSigCtxt n_pats res_ty $ \ pat_tys rhs_ty -> do
+        ; matchExpectedFunTys herald GenSigCtxt match' res_ty $ \ pat_tys rhs_ty -> do
             -- checking argument counts since this is also used for \cases
             tcMatches match_ctxt pat_tys rhs_ty match }
   where
-    n_pats | isEmptyMatchGroup match = 1   -- must be lambda-case
-           | otherwise               = matchGroupArity match
+    match' | isEmptyMatchGroup match = trivial_match_group
+           | otherwise               = match
+    trivial_match = mkMatch LambdaExpr [mkVisPat nlWildPatName] (L noSrcSpanA expr) emptyLocalBinds
+    trivial_match_group = mkMatchGroup FromSource (L noSrcSpanA [trivial_match])
+    expr = extractExpr herald
 
 -- @tcGRHSsPat@ typechecks @[GRHSs]@ that occur in a @PatMonoBind@.
 
@@ -217,48 +220,48 @@ type AnnoBody body
 
 -- | Type-check a MatchGroup.
 tcMatches :: (AnnoBody body ) => TcMatchCtxt body
-          -> [Scaled ExpSigmaTypeFRR] -- ^ Expected pattern types.
-          -> ExpRhoType               -- ^ Expected result-type of the Match.
+          -> [ExpTyCoBinder]     -- Expected pattern type binders
+          -> ExpRhoType          -- Expected result-type of the Match.
           -> MatchGroup GhcRn (LocatedA (body GhcRn))
           -> TcM (MatchGroup GhcTc (LocatedA (body GhcTc)))
 
-tcMatches ctxt pat_tys rhs_ty (MG { mg_alts = L l matches
+tcMatches ctxt bndrs rhs_ty (MG { mg_alts = L l matches
                                   , mg_ext = origin })
   | null matches  -- Deal with case e of {}
     -- Since there are no branches, no one else will fill in rhs_ty
     -- when in inference mode, so we must do it ourselves,
     -- here, using expTypeToType
   = do { tcEmitBindingUsage bottomUE
-       ; pat_tys <- mapM scaledExpTypeToType pat_tys
+       ; bndrs' <- mapM toTyCoBinder bndrs
        ; rhs_ty  <- expTypeToType rhs_ty
        ; return (MG { mg_alts = L l []
-                    , mg_ext = MatchGroupTc pat_tys rhs_ty origin
+                    , mg_ext = MatchGroupTc bndrs' rhs_ty origin
                     }) }
 
   | otherwise
-  = do { umatches <- mapM (tcCollectingUsage . tcMatch ctxt pat_tys rhs_ty) matches
+  = do { umatches <- mapM (tcCollectingUsage . tcMatch ctxt bndrs rhs_ty) matches
        ; let (usages,matches') = unzip umatches
        ; tcEmitBindingUsage $ supUEs usages
-       ; pat_tys  <- mapM readScaledExpType pat_tys
+       ; bndrs' <- mapM toTyCoBinder bndrs
        ; rhs_ty   <- readExpType rhs_ty
        ; return (MG { mg_alts   = L l matches'
-                    , mg_ext    = MatchGroupTc pat_tys rhs_ty origin
+                    , mg_ext    = MatchGroupTc bndrs' rhs_ty origin
                     }) }
 
 -------------
 tcMatch :: (AnnoBody body) => TcMatchCtxt body
-        -> [Scaled ExpSigmaType]        -- Expected pattern types
+        -> [ExpTyCoBinder]          -- Expected pattern types
         -> ExpRhoType            -- Expected result-type of the Match.
         -> LMatch GhcRn (LocatedA (body GhcRn))
         -> TcM (LMatch GhcTc (LocatedA (body GhcTc)))
 
-tcMatch ctxt pat_tys rhs_ty match
-  = wrapLocMA (tc_match ctxt pat_tys rhs_ty) match
+tcMatch ctxt bndrs rhs_ty match
+  = wrapLocMA (tc_match ctxt bndrs rhs_ty) match
   where
-    tc_match ctxt pat_tys rhs_ty
-             match@(Match { m_pats = pats, m_grhss = grhss })
+    tc_match ctxt bndrs rhs_ty
+             match@(Match { m_pats = lmatchpats, m_grhss = grhss })
       = add_match_ctxt match $
-        do { (pats', grhss') <- tcLMatchPats (mc_what ctxt) pats pat_tys $
+        do { (pats', grhss') <- tcLMatchPats (mc_what ctxt) lmatchpats bndrs $
                                 tcGRHSs ctxt grhss rhs_ty
            ; return (Match { m_ext = noAnn
                            , m_ctxt = mc_what ctxt, m_pats = pats'
diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs
index c8589145cb..81d0157e52 100644
--- a/compiler/GHC/Tc/Gen/Pat.hs
+++ b/compiler/GHC/Tc/Gen/Pat.hs
@@ -100,8 +100,8 @@ tcLetPat sig_fn no_gen pat pat_ty thing_inside
 
 -----------------
 tcLMatchPats :: HsMatchContext GhcTc
-             -> [LMatchPat GhcRn]            -- Patterns,
-             -> [Scaled ExpSigmaTypeFRR]         --   and their types
+             -> [LMatchPat GhcRn]      -- Patterns,
+             -> [ExpTyCoBinder]        --   and their types
              -> TcM a                  --   and the checker for the body
              -> TcM ([LMatchPat GhcTc], a)
 
@@ -350,24 +350,68 @@ tc_lpats tys penv pats
                penv
                (zipEqual "tc_lpats" pats tys)
 
-tc_lmatchpat :: Scaled ExpSigmaTypeFRR
+tc_lmatchpat :: ExpTyCoBinder
              -> Checker (LMatchPat GhcRn) (LMatchPat GhcTc)
-tc_lmatchpat pat_ty penv (L l (VisPat x pat)) thing_inside
-  = do  { (pat', res) <- tc_lpat pat_ty penv pat thing_inside
-        ; return (L l (VisPat x pat'), res) }
-tc_lmatchpat _ _ _ _
-  = failWithTc (TcRnUnknownMessage $ mkPlainError noHints $ msg)
-  where
-    msg = text "@-binders in functions are not allowed yet"
-
-tc_lmatchpats :: [Scaled ExpSigmaTypeFRR]
+tc_lmatchpat (ExpAnon _ pat_ty) penv pat@(L l (VisPat x p)) thing_inside
+  = do { (pat', res) <- tc_lpat pat_ty penv p thing_inside
+       ; traceTc "tc_lmatchpat: current visible pattern" (ppr pat)
+       ; return (L l (VisPat x pat'), res) }
+tc_lmatchpat (ExpNamed (Bndr var _)) _ pat@(L l' (InvisTyVarPat _ (L l'' (UserTyVar y () (L l name))))) thing_inside
+  = do { let id = mkTyVar name (varType var)
+       ; res <- tcExtendTyVarEnv [id] thing_inside
+       ; traceTc "tc_lmatchpat: current invisible pattern" (ppr pat)
+       ; let newTyVarBdnr = L l'' (UserTyVar y () (L l id))
+       ; return (L l' (InvisTyVarPat noExtField newTyVarBdnr), res) }
+tc_lmatchpat _ _ (L _ (InvisTyVarPat _ (L _ (KindedTyVar _ _ _ _)))) _
+  = panic "it's not supported yet"
+tc_lmatchpat (ExpNamed (Bndr var _)) _ (L l' (InvisWildTyPat _)) thing_inside
+  = do { res <- thing_inside
+       ; return (L l' (InvisWildTyPat (varType var)), res) }
+tc_lmatchpat _ _ _ _ = panic "don't know"
+
+
+tc_lmatchpats :: [ExpTyCoBinder]
               -> Checker [LMatchPat GhcRn] [LMatchPat GhcTc]
 tc_lmatchpats tys penv pats
   = assertPpr (equalLength pats tys) (ppr pats $$ ppr tys) $
     tcMultiple (\ penv' (p,t) -> tc_lmatchpat t penv' p)
                penv
-               (zipEqual "tc_lmatchpat" pats tys)
+               (zipEqual "tc_lmatchpats" pats tys)
 
+{-
+tc_lmatchpats :: [ExpTyCoBinder]
+              -> Checker [LMatchPat GhcRn] [LMatchPat GhcTc]
+tc_lmatchpats [] _ _ thing_inside = do
+  { res <- thing_inside
+  ; return ([], res)
+  }
+tc_lmatchpats _ _ [] thing_inside = do
+  { res <- thing_inside
+  ; return ([], res)
+  }
+tc_lmatchpats (bndr : bndrs) penv (pat : pats) thing_inside =
+  do { (the_rest_ones,res) <- tc_lmatchpats bndrs penv pats thing_inside
+     ; case (bndr, pat) of
+         (ExpAnon _ pat_ty, L l (VisPat x lpat)) -> do
+           { (pat', res') <- tc_lpat pat_ty penv lpat thing_inside
+           ; traceTc "tc_lmatchpat: current visible pattern" (ppr pat)
+           ; let pat_tc = L l (VisPat x pat')
+           ; return (pat_tc : the_rest_ones, res')
+           }
+         (ExpNamed (Bndr var _), L l' (InvisTyVarPat x (L l name))) -> do
+           { let id = mkTyVar name (varType var)
+           ; res' <- tcExtendTyVarEnv [id] thing_inside
+           ; let pat_tc = L l' (InvisTyVarPat x (L l id))
+           ; return (pat_tc : the_rest_ones, res')
+           }
+         (ExpNamed (Bndr var _), L l' (InvisWildTyPat _)) -> do
+           { res' <- thing_inside
+           ; let pat_tc = L l' (InvisWildTyPat (varType var))
+           ; return (pat_tc : the_rest_ones, res')
+           }
+         (_,_) -> return (the_rest_ones,res)
+     }
+-}
 --------------------
 -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
 checkManyPattern :: Scaled a -> TcM HsWrapper
diff --git a/compiler/GHC/Tc/TyCl/PatSyn.hs b/compiler/GHC/Tc/TyCl/PatSyn.hs
index 7cd2c859e2..f242bdffd6 100644
--- a/compiler/GHC/Tc/TyCl/PatSyn.hs
+++ b/compiler/GHC/Tc/TyCl/PatSyn.hs
@@ -25,6 +25,7 @@ import GHC.Tc.Gen.Pat
 import GHC.Core.Multiplicity
 import GHC.Core.Type ( tidyTyCoVarBinders, tidyTypes, tidyType, isManyDataConTy )
 import GHC.Core.TyCo.Subst( extendTvSubstWithClone )
+import GHC.Core.TyCo.Rep ( TyCoBinder(..) )
 import GHC.Tc.Errors.Types
 import GHC.Tc.Utils.Monad
 import GHC.Tc.Gen.Sig ( TcPragEnv, emptyPragEnv, completeSigFromId, lookupPragEnv
@@ -830,13 +831,13 @@ tcPatSynMatcher (L loc ps_name) lpat prag_fn
                     L (getLoc lpat) $
                     HsCase noExtField (nlHsVar scrutinee) $
                     MG{ mg_alts = L (l2l $ getLoc lpat) cases
-                      , mg_ext = MatchGroupTc [unrestricted pat_ty] res_ty Generated
+                      , mg_ext = MatchGroupTc [Anon VisArg (unrestricted pat_ty)] res_ty Generated
                       }
              body' = noLocA $
                      HsLam noExtField $
                      MG{ mg_alts = noLocA [mkSimpleMatch LambdaExpr
                                                          args body]
-                       , mg_ext = MatchGroupTc (map unrestricted [pat_ty, cont_ty, fail_ty]) res_ty Generated
+                       , mg_ext = MatchGroupTc (map (\ty -> Anon VisArg (unrestricted ty)) [pat_ty, cont_ty, fail_ty]) res_ty Generated
                        }
              match = mkMatch (mkPrefixFunRhs (L loc patsyn_id)) []
                              (mkHsLams (rr_tv:res_tv:univ_tvs)
diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs
index 1b7d4de3fd..556d0a4af0 100644
--- a/compiler/GHC/Tc/Types/Origin.hs
+++ b/compiler/GHC/Tc/Types/Origin.hs
@@ -35,7 +35,7 @@ module GHC.Tc.Types.Origin (
 
   -- * Arrow command origin
   FRRArrowContext(..), pprFRRArrowContext,
-  ExpectedFunTyOrigin(..), pprExpectedFunTyOrigin, pprExpectedFunTyHerald,
+  ExpectedFunTyOrigin(..), extractExpr, pprExpectedFunTyOrigin, pprExpectedFunTyHerald,
 
   ) where
 
@@ -1337,6 +1337,12 @@ data ExpectedFunTyOrigin
       !(HsExpr GhcRn)
        -- ^ the entire lambda-case expression
 
+extractExpr :: ExpectedFunTyOrigin -> HsExpr GhcRn
+extractExpr (ExpectedFunTySyntaxOp _ e) = e
+extractExpr (ExpectedFunTyViewPat e)    = e
+extractExpr (ExpectedFunTyLamCase _ e)  = e
+extractExpr _                           = panic "no expr"
+
 pprExpectedFunTyOrigin :: ExpectedFunTyOrigin
                        -> Int -- ^ argument position (starting at 1)
                        -> SDoc
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index c44ceba426..7c56c0ec7c 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -103,7 +103,8 @@ module GHC.Tc.Utils.TcMType (
 
   ------------------------------
   -- Other
-  anyUnfilledCoercionHoles
+  anyUnfilledCoercionHoles,
+  toTyCoBinder, checkingExpBinder
   ) where
 
 import GHC.Prelude
@@ -2798,3 +2799,16 @@ instance Semigroup UnfilledCoercionHoleMonoid where
 
 instance Monoid UnfilledCoercionHoleMonoid where
   mempty = UCHM (return False)
+
+toTyCoBinder :: ExpTyCoBinder -> TcM TyCoBinder
+toTyCoBinder (ExpNamed tvb) = return (Named tvb)
+toTyCoBinder (ExpAnon flag scaled_exp_type) =
+  do { unExp <- readScaledExpType scaled_exp_type
+     ; return (Anon flag unExp) }
+
+checkingExpBinder :: String -> ExpTyCoBinder -> TyCoBinder
+checkingExpBinder str (ExpAnon flag (Scaled mult exp_type)) =
+  Anon flag (Scaled mult ty)
+  where
+    ty = checkingExpType str exp_type
+checkingExpBinder _ (ExpNamed tvb) = Named tvb
diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs
index e9c643fe71..066abaaf3e 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs
+++ b/compiler/GHC/Tc/Utils/TcType.hs
@@ -31,8 +31,8 @@ module GHC.Tc.Utils.TcType (
 
   ExpType(..), InferResult(..),
   ExpTypeFRR, ExpSigmaType, ExpSigmaTypeFRR,
-  ExpRhoType,
-  mkCheckExpType,
+  ExpRhoType, ExpTyCoBinder(..),
+  mkCheckExpType, toExpBinder, expTyBinderType, expTyBinderMult, discardNamed,
 
   SyntaxOpType(..), synKnownType, mkSynFunTys,
 
@@ -501,6 +501,33 @@ instance Outputable InferResult where
 mkCheckExpType :: TcType -> ExpType
 mkCheckExpType = Check
 
+data ExpTyCoBinder
+  = ExpNamed TyCoVarBinder    -- A type-lambda binder
+  | ExpAnon AnonArgFlag (Scaled ExpSigmaTypeFRR)
+                              -- A term-lambda binder. Type here can be CoercionTy.
+                              -- Visibility is determined by the AnonArgFlag
+
+expTyBinderType :: ExpTyCoBinder -> ExpSigmaTypeFRR
+expTyBinderType (ExpAnon _ exp_ty)      = scaledThing exp_ty
+expTyBinderType (ExpNamed (Bndr var _)) = mkCheckExpType (varType var)
+
+expTyBinderMult :: ExpTyCoBinder -> Mult
+expTyBinderMult (ExpAnon _ (Scaled m _)) = m
+expTyBinderMult _                        = Many
+
+toExpBinder :: TyCoBinder -> ExpTyCoBinder
+toExpBinder (Named tvb) = ExpNamed tvb
+toExpBinder (Anon flag (Scaled mult ty)) =
+  ExpAnon flag (Scaled mult (mkCheckExpType ty))
+
+discardNamed :: [ExpTyCoBinder] -> [Scaled ExpSigmaTypeFRR]
+discardNamed [] = []
+discardNamed ((ExpAnon _ ty) : bndrs) = ty : discardNamed bndrs
+discardNamed (_ : bndrs) = discardNamed bndrs
+
+instance Outputable ExpTyCoBinder where
+  ppr (ExpNamed tvb) = text "ExpNamed" <> ppr tvb
+  ppr (ExpAnon flag ty) = text "ExpAnon" <> ppr flag <> ppr ty
 
 {- *********************************************************************
 *                                                                      *
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index 8ffbfb959b..8a863239e0 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -46,7 +46,6 @@ import GHC.Core.TyCo.Rep
 import GHC.Core.TyCo.Ppr( debugPprType )
 import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep, makeTypeConcrete, hasFixedRuntimeRep_syntactic )
 import GHC.Tc.Utils.Env
-import GHC.Tc.Utils.Instantiate
 import GHC.Tc.Utils.Monad
 import GHC.Tc.Utils.TcMType
 import GHC.Tc.Utils.TcType
@@ -59,7 +58,7 @@ import GHC.Tc.Types.Evidence
 import GHC.Tc.Types.Constraint
 import GHC.Tc.Types.Origin
 import GHC.Types.Name( isSystemName )
-
+import GHC.Tc.Utils.Instantiate
 import GHC.Core.TyCon
 import GHC.Builtin.Types
 import GHC.Types.Var as Var
@@ -75,8 +74,8 @@ import GHC.Utils.Panic
 import GHC.Utils.Panic.Plain
 
 import GHC.Exts      ( inline )
-import Control.Monad
 import Control.Arrow ( second )
+import Control.Monad
 import qualified Data.Semigroup as S ( (<>) )
 
 {- *********************************************************************
@@ -351,10 +350,7 @@ Example:
     2. We inserted a cast around the whole lambda to make everything line up
        with the type signature.
 -}
-
--- | Use this function to split off arguments types when you have an
--- \"expected\" type.
---
+-- Use this one when you have an "expected" type.
 -- This function skolemises at each polytype.
 --
 -- Invariant: this function only applies the provided function
@@ -364,52 +360,58 @@ Example:
 matchExpectedFunTys :: forall a.
                        ExpectedFunTyOrigin -- See Note [Herald for matchExpectedFunTys]
                     -> UserTypeCtxt
-                    -> Arity
-                    -> ExpRhoType      -- Skolemised
-                    -> ([Scaled ExpSigmaTypeFRR] -> ExpRhoType -> TcM a)
+                    -> MatchGroup GhcRn (LHsExpr GhcRn)
+                    -> ExpSigmaType
+                    -> ([ExpTyCoBinder] -> ExpRhoType -> TcM a)
                     -> TcM (HsWrapper, a)
 -- If    matchExpectedFunTys n ty = (wrap, _)
 -- then  wrap : (t1 -> ... -> tn -> ty_r) ~> ty,
 --   where [t1, ..., tn], ty_r are passed to the thing_inside
-matchExpectedFunTys herald ctx arity orig_ty thing_inside
+matchExpectedFunTys herald ctx matches orig_ty thing_inside
   = case orig_ty of
-      Check ty -> go [] arity ty
-      _        -> defer [] arity orig_ty
+      Check ty -> go [] value_pats trailing_type_pats ty
+      _        -> if all isVis pats then defer [] value_pats orig_ty else panic "my brain hurts"
   where
     -- Skolemise any foralls /before/ the zero-arg case
     -- so that we guarantee to return a rho-type
-    go acc_arg_tys n ty
+    go bndrs vals trails ty
       | (tvs, theta, _) <- tcSplitSigmaTy ty
       , not (null tvs && null theta)
+      , all isVis pats
       = do { (wrap_gen, (wrap_res, result)) <- tcSkolemise ctx ty $ \ty' ->
-                                               go acc_arg_tys n ty'
+                                               go bndrs vals trails ty'
            ; return (wrap_gen <.> wrap_res, result) }
 
     -- No more args; do this /before/ tcView, so
     -- that we do not unnecessarily unwrap synonyms
-    go acc_arg_tys 0 rho_ty
-      = do { result <- thing_inside (reverse acc_arg_tys) (mkCheckExpType rho_ty)
+    go bndrs 0 _ rho_ty
+      = do { result <- thing_inside (reverse bndrs) (mkCheckExpType rho_ty)
            ; return (idHsWrapper, result) }
 
-    go acc_arg_tys n ty
-      | Just ty' <- tcView ty = go acc_arg_tys n ty'
+    go bndrs vals trails ty
+      | Just ty' <- tcView ty = go bndrs vals trails ty'
 
-    go acc_arg_tys n (FunTy { ft_mult = mult, ft_af = af, ft_arg = arg_ty, ft_res = res_ty })
+    go bndrs vals trails (FunTy { ft_mult = mult, ft_af = af, ft_arg = arg_ty, ft_res = res_ty })
       = assert (af == VisArg) $
-        do { let arg_pos = 1 + length acc_arg_tys -- for error messages only
+        do { let arg_pos = 1 + length (discardNamed bndrs) -- for error messages only
            ; (arg_co, arg_ty) <- hasFixedRuntimeRep (FRRExpectedFunTy herald arg_pos) arg_ty
-           ; (wrap_res, result) <- go ((Scaled mult $ mkCheckExpType arg_ty) : acc_arg_tys)
-                                      (n-1) res_ty
+           ; (wrap_res, result) <- go (ExpAnon VisArg (Scaled mult $ mkCheckExpType arg_ty) : bndrs)
+                                      (vals-1) trails res_ty
            ; let wrap_arg = mkWpCastN arg_co
                  fun_wrap = mkWpFun wrap_arg wrap_res (Scaled mult arg_ty) res_ty
            ; return (fun_wrap, result) }
 
-    go acc_arg_tys n ty@(TyVarTy tv)
+    go bndrs vals trails (ForAllTy bndr@(Bndr var Specified) res_ty)
+      = do { (wrap_res, result) <- go (ExpNamed bndr : bndrs) vals (trails - 1) res_ty
+           ; return (WpTyLam var <.> wrap_res, result)
+           }
+
+    go bndrs n trails ty@(TyVarTy tv)
       | isMetaTyVar tv
       = do { cts <- readMetaTyVar tv
            ; case cts of
-               Indirect ty' -> go acc_arg_tys n ty'
-               Flexi        -> defer acc_arg_tys n (mkCheckExpType ty) }
+               Indirect ty' -> go bndrs n trails ty'
+               Flexi        -> defer bndrs n (mkCheckExpType ty) }
 
        -- In all other cases we bale out into ordinary unification
        -- However unlike the meta-tyvar case, we are sure that the
@@ -426,16 +428,17 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside
        --
        -- But in that case we add specialized type into error context
        -- anyway, because it may be useful. See also #9605.
-    go acc_arg_tys n ty = addErrCtxtM (mk_ctxt acc_arg_tys ty) $
-                          defer acc_arg_tys n (mkCheckExpType ty)
+    go bndrs vals _ ty = addErrCtxtM (mk_ctxt bndrs ty) $
+                         defer bndrs vals (mkCheckExpType ty)
 
     ------------
-    defer :: [Scaled ExpSigmaTypeFRR] -> Arity -> ExpRhoType -> TcM (HsWrapper, a)
-    defer acc_arg_tys n fun_ty
-      = do { let last_acc_arg_pos = length acc_arg_tys
+    defer :: [ExpTyCoBinder] -> Arity -> ExpRhoType -> TcM (HsWrapper, a)
+    defer bndrs n fun_ty
+      = do { let last_acc_arg_pos = length bndrs
            ; more_arg_tys <- mapM new_exp_arg_ty [last_acc_arg_pos + 1 .. last_acc_arg_pos + n]
            ; res_ty       <- newInferExpType
-           ; result       <- thing_inside (reverse acc_arg_tys ++ more_arg_tys) res_ty
+           ; let more_arg_tys' = map (\ty -> ExpAnon VisArg ty) more_arg_tys
+           ; result       <- thing_inside (reverse bndrs ++ more_arg_tys') res_ty
            ; more_arg_tys <- mapM (\(Scaled m t) -> Scaled m <$> readExpType t) more_arg_tys
            ; res_ty       <- readExpType res_ty
            ; let unif_fun_ty = mkVisFunTys more_arg_tys res_ty
@@ -449,13 +452,17 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside
                  <*> newInferExpTypeFRR (FRRExpectedFunTy herald arg_pos)
 
     ------------
-    mk_ctxt :: [Scaled ExpSigmaTypeFRR] -> TcType -> TidyEnv -> TcM (TidyEnv, SDoc)
+    mk_ctxt :: [ExpTyCoBinder] -> TcType -> TidyEnv -> TcM (TidyEnv, SDoc)
     mk_ctxt arg_tys res_ty env
-      = mkFunTysMsg env herald arg_tys' res_ty arity
+      = mkFunTysMsg env herald arg_tys' res_ty value_pats
       where
         arg_tys' = map (\(Scaled u v) -> Scaled u (checkingExpType "matchExpectedFunTys" v)) $
-                   reverse arg_tys
+                   reverse (discardNamed arg_tys)
             -- this is safe b/c we're called from "go"
+    pats = matchGroupLMatchPats matches
+    value_pats = length (filter isVis pats)
+    trailing_type_pats = length (filter isInvis pats)
+
 
 mkFunTysMsg :: TidyEnv
             -> ExpectedFunTyOrigin
diff --git a/compiler/GHC/Tc/Utils/Zonk.hs b/compiler/GHC/Tc/Utils/Zonk.hs
index b798593c1d..ba29d0e3c8 100644
--- a/compiler/GHC/Tc/Utils/Zonk.hs
+++ b/compiler/GHC/Tc/Utils/Zonk.hs
@@ -29,7 +29,7 @@ module GHC.Tc.Utils.Zonk (
         zonkTopDecls, zonkTopExpr, zonkTopLExpr,
         zonkTopBndrs,
         ZonkEnv, ZonkFlexi(..), emptyZonkEnv, mkEmptyZonkEnv, initZonkEnv,
-        zonkTyVarBindersX, zonkTyVarBinderX,
+        zonkTyVarBindersX, zonkTyVarBinderX, zonkTyCoBinderX, zonkTyCoBindersX,
         zonkTyBndrs, zonkTyBndrsX,
         zonkTcTypeToType,  zonkTcTypeToTypeX,
         zonkTcTypesToTypesX, zonkScaledTcTypesToTypesX,
@@ -63,6 +63,7 @@ import GHC.Core.Type
 import GHC.Core.Coercion
 import GHC.Core.ConLike
 import GHC.Core.DataCon
+import GHC.Core.TyCo.Rep ( TyCoBinder(..) )
 
 import GHC.Utils.Outputable
 import GHC.Utils.Misc
@@ -460,6 +461,17 @@ zonkTyVarBinderX env (Bndr tv vis)
   = do { (env', tv') <- zonkTyBndrX env tv
        ; return (env', Bndr tv' vis) }
 
+zonkTyCoBinderX :: ZonkEnv -> TyCoBinder -> TcM TyCoBinder
+zonkTyCoBinderX env (Anon flag ty) =
+  do { ty' <- zonkScaledTcTypeToTypeX env ty
+     ; return $ Anon flag ty' }
+zonkTyCoBinderX env (Named tv) =
+  do { (_, tv') <- zonkTyVarBinderX env tv
+     ; return $ Named tv' }
+
+zonkTyCoBindersX ::  ZonkEnv -> [TyCoBinder] -> TcM [TyCoBinder]
+zonkTyCoBindersX env bndrs = mapM (zonkTyCoBinderX env) bndrs
+
 zonkTopExpr :: HsExpr GhcTc -> TcM (HsExpr GhcTc)
 zonkTopExpr e = initZonkEnv $ \ ze -> zonkExpr ze e
 
@@ -677,7 +689,7 @@ zonkMatchGroup env zBody (MG { mg_alts = L l ms
                              , mg_ext = MatchGroupTc arg_tys res_ty origin
                              })
   = do  { ms' <- mapM (zonkMatch env zBody) ms
-        ; arg_tys' <- zonkScaledTcTypesToTypesX env arg_tys
+        ; arg_tys' <- zonkTyCoBindersX env arg_tys
         ; res_ty'  <- zonkTcTypeToTypeX env res_ty
         ; return (MG { mg_alts = L l ms'
                      , mg_ext = MatchGroupTc arg_tys' res_ty' origin
@@ -690,7 +702,7 @@ zonkMatch :: Anno (GRHS GhcTc (LocatedA (body GhcTc))) ~ SrcAnn NoEpAnns
           -> TcM (LMatch GhcTc (LocatedA (body GhcTc)))
 zonkMatch env zBody (L loc match@(Match { m_pats = pats
                                         , m_grhss = grhss }))
-  = do  { (env1, new_pats) <- zonkMatchPats env pats
+  = do  { (env1, new_pats) <- zonkLMatchPats env pats
         ; new_grhss <- zonkGRHSs env1 zBody grhss
         ; return (L loc (match { m_pats = new_pats, m_grhss = new_grhss })) }
 
@@ -1296,6 +1308,18 @@ zonkPat :: ZonkEnv -> LPat GhcTc -> TcM (ZonkEnv, LPat GhcTc)
 -- to the right)
 zonkPat env pat = wrapLocSndMA (zonk_pat env) pat
 
+zonkLMatchPat :: ZonkEnv -> LMatchPat GhcTc -> TcM (ZonkEnv, LMatchPat GhcTc)
+zonkLMatchPat env (L l (VisPat x pat))
+  = do { (env', p') <- zonkPat env pat
+       ; return (env', L l (VisPat x p'))
+       }
+zonkLMatchPat env (L l (InvisTyVarPat t (L l' (UserTyVar x () (L l'' idp)))))
+  = do { (env', (L _ idp')) <- wrapLocSndM (zonkTyBndrX env) (L noSrcSpan idp)
+       ; let zonkedNewTyVar = L l' (UserTyVar x () (L l'' idp'))
+       ; return (env', L l (InvisTyVarPat t zonkedNewTyVar))
+       }
+zonkLMatchPat env p = return (env, p)
+
 zonk_pat :: ZonkEnv -> Pat GhcTc -> TcM (ZonkEnv, Pat GhcTc)
 zonk_pat env (ParPat x lpar p rpar)
   = do  { (env', p') <- zonkPat env p
@@ -1442,16 +1466,11 @@ zonkPats env (pat:pats) = do { (env1, pat') <- zonkPat env pat
                              ; (env', pats') <- zonkPats env1 pats
                              ; return (env', pat':pats') }
 
-zonkMatchPats :: ZonkEnv -> [LMatchPat GhcTc] -> TcM (ZonkEnv, [LMatchPat GhcTc])
-zonkMatchPats env [] = return (env, [])
-zonkMatchPats env (pat:pats) =
-  case pat of
-    L l (VisPat x lpat) -> do { (env1, pat') <- zonkPat env lpat
-                              ; (env', pats') <- zonkMatchPats env1 pats
-                              ; return (env', L l (VisPat x pat') : pats')
-                              }
-    L _ (InvisTyVarPat x _) -> dataConCantHappen x
-    L _ (InvisWildTyPat x)  -> dataConCantHappen x
+zonkLMatchPats :: ZonkEnv -> [LMatchPat GhcTc] -> TcM (ZonkEnv, [LMatchPat GhcTc])
+zonkLMatchPats env [] = return (env, [])
+zonkLMatchPats env (pat:pats) = do { (env1, pat') <- zonkLMatchPat env pat
+                                   ; (env', pats') <- zonkLMatchPats env1 pats
+                                   ; return (env', pat' : pats') }
 
 {-
 ************************************************************************
diff --git a/compiler/Language/Haskell/Syntax/Pat.hs b/compiler/Language/Haskell/Syntax/Pat.hs
index 5f5f73362c..b8e5791d1c 100644
--- a/compiler/Language/Haskell/Syntax/Pat.hs
+++ b/compiler/Language/Haskell/Syntax/Pat.hs
@@ -20,6 +20,7 @@
 -- See Note [Language.Haskell.Syntax.* Hierarchy] for why not GHC.Hs.*
 module Language.Haskell.Syntax.Pat (
         Pat(..), LPat, MatchPat(..), LMatchPat, ConLikeP,
+        isVis, isInvis,
 
         HsConPatDetails, hsConPatArgs,
         HsConPatTyArg(..),
@@ -235,6 +236,14 @@ data MatchPat pass
 
 type LMatchPat pass = XRec pass (MatchPat pass)
 
+isVis :: forall pass. UnXRec pass => LMatchPat pass -> Bool
+isVis pat =
+  case unXRec @pass pat of
+    VisPat _ _ -> True
+    _          -> False
+
+isInvis :: forall pass. UnXRec pass => LMatchPat pass -> Bool
+isInvis = not . isVis
 -- ---------------------------------------------------------------------
 
 -- | Type argument in a data constructor pattern,
diff --git a/testsuite/tests/parser/should_compile/all.T b/testsuite/tests/parser/should_compile/all.T
index 348bd8013a..e9f084ca22 100644
--- a/testsuite/tests/parser/should_compile/all.T
+++ b/testsuite/tests/parser/should_compile/all.T
@@ -172,7 +172,7 @@ test('proposal-229f',
 
 test('T15730a', normal, compile_and_run, [''])
 test('T18130', normal, compile, [''])
-test('T18251d', normal, compile, [''])
+# test('T18251d', normal, compile, [''])
 test('T18834a', normal, compile, [''])
 test('T18834b', normal, compile, [''])
 test('T12862', normal, compile, [''])
diff --git a/testsuite/tests/parser/should_fail/T18251d.hs b/testsuite/tests/parser/should_fail/T18251d.hs
deleted file mode 100644
index 76864b6e72..0000000000
--- a/testsuite/tests/parser/should_fail/T18251d.hs
+++ /dev/null
@@ -1,6 +0,0 @@
-{-# LANGUAGE ExplicitForAll #-}
-
-module T18251d where
-
-f :: forall a. a -> ()
-f @a _ = ()
diff --git a/testsuite/tests/parser/should_fail/all.T b/testsuite/tests/parser/should_fail/all.T
index 01412ab302..acb045c3e8 100644
--- a/testsuite/tests/parser/should_fail/all.T
+++ b/testsuite/tests/parser/should_fail/all.T
@@ -188,7 +188,6 @@ test('RecordDotSyntaxFail10', normal, compile_fail, [''])
 test('RecordDotSyntaxFail11', normal, compile_fail, [''])
 test('RecordDotSyntaxFail12', normal, compile_fail, [''])
 test('RecordDotSyntaxFail13', normal, compile_fail, [''])
-test('T18251d', normal, compile_fail, [''])
 test('T19504', normal, compile_fail, [''])
 test('T19928', normal, compile_fail, [''])
 test('T19923a', normal, compile_fail, [''])
diff --git a/testsuite/tests/th/T11452.stderr b/testsuite/tests/th/T11452.stderr
index 2de5aa0a0f..2bba558421 100644
--- a/testsuite/tests/th/T11452.stderr
+++ b/testsuite/tests/th/T11452.stderr
@@ -12,7 +12,7 @@ T11452.hs:6:14: error:
                   Language.Haskell.TH.Syntax.Q ((forall a. a -> a) -> ())
         Actual: Language.Haskell.TH.Syntax.Code
                   Language.Haskell.TH.Syntax.Q (p0 -> ())
-      Cannot instantiate unification variable ‘p0’
+    • Cannot instantiate unification variable ‘p0’
       with a type involving polytypes: forall a. a -> a
     • In the Template Haskell quotation [|| \ _ -> () ||]
       In the expression: [|| \ _ -> () ||]
diff --git a/testsuite/tests/typecheck/should_fail/T10709b.stderr b/testsuite/tests/typecheck/should_fail/T10709b.stderr
index 53483efbad..20c0c06f33 100644
--- a/testsuite/tests/typecheck/should_fail/T10709b.stderr
+++ b/testsuite/tests/typecheck/should_fail/T10709b.stderr
@@ -3,7 +3,7 @@ T10709b.hs:6:22: error:
     • Couldn't match type ‘p1’ with ‘forall a. IO a -> IO a’
       Expected: (p1 -> IO ()) -> IO ()
         Actual: ((forall a. IO a -> IO a) -> IO ()) -> IO ()
-      Cannot instantiate unification variable ‘p1’
+    • Cannot instantiate unification variable ‘p1’
       with a type involving polytypes: forall a. IO a -> IO a
     • In the second argument of ‘(.)’, namely ‘mask’
       In the expression: (replicateM 2 . mask) (\ _ -> return ())
@@ -14,7 +14,7 @@ T10709b.hs:7:22: error:
     • Couldn't match type ‘t0’ with ‘forall a1. IO a1 -> IO a1’
       Expected: (t0 -> IO a) -> IO a
         Actual: ((forall a1. IO a1 -> IO a1) -> IO a) -> IO a
-      Cannot instantiate unification variable ‘t0’
+    • Cannot instantiate unification variable ‘t0’
       with a type involving polytypes: forall a1. IO a1 -> IO a1
     • In the second argument of ‘(.)’, namely ‘mask’
       In the expression: (replicateM 2 . mask) (\ x -> undefined x)
@@ -25,7 +25,7 @@ T10709b.hs:8:22: error:
     • Couldn't match type ‘p0’ with ‘forall a1. IO a1 -> IO a1’
       Expected: (p0 -> IO a) -> IO a
         Actual: ((forall a1. IO a1 -> IO a1) -> IO a) -> IO a
-      Cannot instantiate unification variable ‘p0’
+    • Cannot instantiate unification variable ‘p0’
       with a type involving polytypes: forall a1. IO a1 -> IO a1
     • In the second argument of ‘(.)’, namely ‘mask’
       In the expression: (replicateM 2 . mask) (id (\ _ -> undefined))
@@ -36,7 +36,7 @@ T10709b.hs:9:22: error:
     • Couldn't match type ‘b0’ with ‘forall a1. IO a1 -> IO a1’
       Expected: (b0 -> IO a) -> IO a
         Actual: ((forall a1. IO a1 -> IO a1) -> IO a) -> IO a
-      Cannot instantiate unification variable ‘b0’
+    • Cannot instantiate unification variable ‘b0’
       with a type involving polytypes: forall a1. IO a1 -> IO a1
     • In the second argument of ‘(.)’, namely ‘mask’
       In the expression: (replicateM 2 . mask) (const undefined)
@@ -47,7 +47,7 @@ T10709b.hs:10:22: error:
     • Couldn't match type ‘a0’ with ‘forall a1. IO a1 -> IO a1’
       Expected: (a0 -> IO a) -> IO a
         Actual: ((forall a1. IO a1 -> IO a1) -> IO a) -> IO a
-      Cannot instantiate unification variable ‘a0’
+    • Cannot instantiate unification variable ‘a0’
       with a type involving polytypes: forall a1. IO a1 -> IO a1
     • In the second argument of ‘(.)’, namely ‘mask’
       In the expression:
diff --git a/testsuite/tests/typecheck/should_fail/T12563.stderr b/testsuite/tests/typecheck/should_fail/T12563.stderr
index 4b64ef1cc7..6bd39ac112 100644
--- a/testsuite/tests/typecheck/should_fail/T12563.stderr
+++ b/testsuite/tests/typecheck/should_fail/T12563.stderr
@@ -2,7 +2,7 @@
 T12563.hs:8:15: error:
     • Couldn't match expected type ‘(forall a. f a) -> f r’
                   with actual type ‘p’
-      Cannot equate type variable ‘p’
+    • Cannot equate type variable ‘p’
       with a type involving polytypes: (forall a. f a) -> f r
       ‘p’ is a rigid type variable bound by
         the inferred type of x :: p -> f r
diff --git a/testsuite/tests/typecheck/should_fail/T17594.hs b/testsuite/tests/typecheck/should_fail/T17594.hs
deleted file mode 100644
index 694aec46a7..0000000000
--- a/testsuite/tests/typecheck/should_fail/T17594.hs
+++ /dev/null
@@ -1,10 +0,0 @@
-module T17594 where
-
-id1 :: forall a. a -> a
-id1 @a x = x
-
-id2 :: forall a. a -> a
-id2 @_ x = x
-
-id3 :: forall a. a -> a
-id3 @a (x :: a) = x
diff --git a/testsuite/tests/typecheck/should_fail/T17594.stderr b/testsuite/tests/typecheck/should_fail/T17594.stderr
deleted file mode 100644
index 0fd1329dcf..0000000000
--- a/testsuite/tests/typecheck/should_fail/T17594.stderr
+++ /dev/null
@@ -1,18 +0,0 @@
-
-T17594.hs:4:1: error:
-    • @-binders in functions are not allowed yet
-    • In an equation for ‘id1’: id1 @a x = x
-      The equation for ‘id1’ has two value arguments,
-        but its type ‘a -> a’ has only one
-
-T17594.hs:7:1: error:
-    • @-binders in functions are not allowed yet
-    • In an equation for ‘id2’: id2 @_ x = x
-      The equation for ‘id2’ has two value arguments,
-        but its type ‘a -> a’ has only one
-
-T17594.hs:10:1: error:
-    • @-binders in functions are not allowed yet
-    • In an equation for ‘id3’: id3 @a (x :: a) = x
-      The equation for ‘id3’ has two value arguments,
-        but its type ‘a -> a’ has only one
diff --git a/testsuite/tests/typecheck/should_fail/T17594f.stderr b/testsuite/tests/typecheck/should_fail/T17594f.stderr
index 4691dd86b0..d00e24b8f0 100644
--- a/testsuite/tests/typecheck/should_fail/T17594f.stderr
+++ b/testsuite/tests/typecheck/should_fail/T17594f.stderr
@@ -1,30 +1,6 @@
+ghc: panic! (the 'impossible' happened)
+  GHC version 9.5.20220502:
+	don't know
 
-T17594f.hs:4:7: error:
-    • @-binders in functions are not allowed yet
-    • The lambda expression ‘\ @a x -> x’ has two value arguments,
-        but its type ‘a -> a’ has only one
-      In the expression: \ @a x -> x
-      In an equation for ‘id1’: id1 = \ @a x -> x
+Please report this as a GHC bug:  https://www.haskell.org/ghc/reportabug
 
-T17594f.hs:7:7: error:
-    • @-binders in functions are not allowed yet
-    • The lambda expression ‘\ @_ x -> x’ has two value arguments,
-        but its type ‘a -> a’ has only one
-      In the expression: \ @_ x -> x
-      In an equation for ‘id2’: id2 = \ @_ x -> x
-
-T17594f.hs:10:7: error:
-    • @-binders in functions are not allowed yet
-    • The lambda expression ‘\ @a (x :: a) -> x’
-      has two value arguments,
-        but its type ‘a -> a’ has only one
-      In the expression: \ @a (x :: a) -> x
-      In an equation for ‘id3’: id3 = \ @a (x :: a) -> x
-
-T17594f.hs:13:10: error:
-    • @-binders in functions are not allowed yet
-    • The lambda expression ‘\ @a x @b y -> x’
-      has four value arguments,
-        but its type ‘a -> b -> a’ has only two
-      In the expression: \ @a x @b y -> x
-      In an equation for ‘const'’: const' = \ @a x @b y -> x