Reject GADT pattern matches in arrow notation

  Tickets #20469 and #20470 showed that the current
  implementation of arrows is not at all up to the task
  of supporting GADTs: GHC produces ill-scoped Core programs
  because it doesn't propagate the evidence introduced by a GADT
  pattern match.

  For the time being, we reject GADT pattern matches in arrow notation.
  Hopefully we are able to add proper support for GADTs in arrows
  in the future.

41 files changed, 376 insertions, 77 deletions

diff --git a/compiler/GHC/Core/ConLike.hs b/compiler/GHC/Core/ConLike.hs
index 868d4a6fed..b375b742f0 100644
--- a/compiler/GHC/Core/ConLike.hs
+++ b/compiler/GHC/Core/ConLike.hs
@@ -9,6 +9,7 @@
 
 module GHC.Core.ConLike (
           ConLike(..)
+        , isVanillaConLike
         , conLikeArity
         , conLikeFieldLabels
         , conLikeInstOrigArgTys
@@ -54,6 +55,12 @@ import qualified Data.Data as Data
 data ConLike = RealDataCon DataCon
              | PatSynCon PatSyn
 
+-- | Is this a \'vanilla\' constructor-like thing
+-- (no existentials, no provided constraints)?
+isVanillaConLike :: ConLike -> Bool
+isVanillaConLike (RealDataCon con) = isVanillaDataCon con
+isVanillaConLike (PatSynCon   ps ) = isVanillaPatSyn  ps
+
 {-
 ************************************************************************
 *                                                                      *
diff --git a/compiler/GHC/Core/PatSyn.hs b/compiler/GHC/Core/PatSyn.hs
index 34a019dce1..c3aeb87c27 100644
--- a/compiler/GHC/Core/PatSyn.hs
+++ b/compiler/GHC/Core/PatSyn.hs
@@ -13,6 +13,7 @@ module GHC.Core.PatSyn (
 
         -- ** Type deconstruction
         patSynName, patSynArity, patSynIsInfix, patSynResultType,
+        isVanillaPatSyn,
         patSynArgs,
         patSynMatcher, patSynBuilder,
         patSynUnivTyVarBinders, patSynExTyVars, patSynExTyVarBinders,
@@ -419,6 +420,10 @@ patSynIsInfix = psInfix
 patSynArity :: PatSyn -> Arity
 patSynArity = psArity
 
+-- | Is this a \'vanilla\' pattern synonym (no existentials, no provided constraints)?
+isVanillaPatSyn :: PatSyn -> Bool
+isVanillaPatSyn ps = null (psExTyVars ps) && null (psProvTheta ps)
+
 patSynArgs :: PatSyn -> [Type]
 patSynArgs = psArgs
 
diff --git a/compiler/GHC/Hs/Expr.hs b/compiler/GHC/Hs/Expr.hs
index 83e36edf54..d6785c2a96 100644
--- a/compiler/GHC/Hs/Expr.hs
+++ b/compiler/GHC/Hs/Expr.hs
@@ -1857,7 +1857,7 @@ instance OutputableBndrId p => Outputable (HsMatchContext (GhcPass p)) where
   ppr LambdaExpr            = text "LambdaExpr"
   ppr CaseAlt               = text "CaseAlt"
   ppr IfAlt                 = text "IfAlt"
-  ppr ProcExpr              = text "ProcExpr"
+  ppr (ArrowMatchCtxt c)    = text "ArrowMatchCtxt" <+> ppr c
   ppr PatBindRhs            = text "PatBindRhs"
   ppr PatBindGuards         = text "PatBindGuards"
   ppr RecUpd                = text "RecUpd"
@@ -1866,6 +1866,11 @@ instance OutputableBndrId p => Outputable (HsMatchContext (GhcPass p)) where
   ppr ThPatQuote            = text "ThPatQuote"
   ppr PatSyn                = text "PatSyn"
 
+instance Outputable HsArrowMatchContext where
+  ppr ProcExpr     = text "ProcExpr"
+  ppr ArrowCaseAlt = text "ArrowCaseAlt"
+  ppr KappaExpr    = text "KappaExpr"
+
 -----------------
 
 instance OutputableBndrId p
@@ -1882,16 +1887,21 @@ matchContextErrString PatBindRhs                 = text "pattern binding"
 matchContextErrString PatBindGuards              = text "pattern binding guards"
 matchContextErrString RecUpd                     = text "record update"
 matchContextErrString LambdaExpr                 = text "lambda"
-matchContextErrString ProcExpr                   = text "proc"
+matchContextErrString (ArrowMatchCtxt c)         = matchArrowContextErrString c
 matchContextErrString ThPatSplice                = panic "matchContextErrString"  -- Not used at runtime
 matchContextErrString ThPatQuote                 = panic "matchContextErrString"  -- Not used at runtime
 matchContextErrString PatSyn                     = panic "matchContextErrString"  -- Not used at runtime
 matchContextErrString (StmtCtxt (ParStmtCtxt c))   = matchContextErrString (StmtCtxt c)
 matchContextErrString (StmtCtxt (TransStmtCtxt c)) = matchContextErrString (StmtCtxt c)
 matchContextErrString (StmtCtxt (PatGuard _))      = text "pattern guard"
-matchContextErrString (StmtCtxt (ArrowExpr))  = text "'do' block"
+matchContextErrString (StmtCtxt (ArrowExpr))       = text "'do' block"
 matchContextErrString (StmtCtxt (HsDoStmt flavour)) = matchDoContextErrString flavour
 
+matchArrowContextErrString :: HsArrowMatchContext -> SDoc
+matchArrowContextErrString ProcExpr     = text "proc"
+matchArrowContextErrString ArrowCaseAlt = text "case"
+matchArrowContextErrString KappaExpr    = text "kappa"
+
 matchDoContextErrString :: HsDoFlavour -> SDoc
 matchDoContextErrString GhciStmtCtxt = text "interactive GHCi command"
 matchDoContextErrString (DoExpr m)   = prependQualified m (text "'do' block")
diff --git a/compiler/GHC/Hs/Instances.hs b/compiler/GHC/Hs/Instances.hs
index 78a663d7fa..21cd9b5d76 100644
--- a/compiler/GHC/Hs/Instances.hs
+++ b/compiler/GHC/Hs/Instances.hs
@@ -366,6 +366,8 @@ deriving instance Data (HsStmtContext GhcPs)
 deriving instance Data (HsStmtContext GhcRn)
 deriving instance Data (HsStmtContext GhcTc)
 
+deriving instance Data HsArrowMatchContext
+
 deriving instance Data HsDoFlavour
 
 deriving instance Data (HsMatchContext GhcPs)
diff --git a/compiler/GHC/HsToCore/Arrows.hs b/compiler/GHC/HsToCore/Arrows.hs
index 5cfd057299..2338e2a451 100644
--- a/compiler/GHC/HsToCore/Arrows.hs
+++ b/compiler/GHC/HsToCore/Arrows.hs
@@ -319,9 +319,9 @@ dsProcExpr pat (L _ (HsCmdTop (CmdTopTc _unitTy cmd_ty ids) cmd)) = do
     let env_ty = mkBigCoreVarTupTy env_ids
     let env_stk_ty = mkCorePairTy env_ty unitTy
     let env_stk_expr = mkCorePairExpr (mkBigCoreVarTup env_ids) mkCoreUnitExpr
-    fail_expr <- mkFailExpr ProcExpr env_stk_ty
+    fail_expr <- mkFailExpr (ArrowMatchCtxt ProcExpr) env_stk_ty
     var <- selectSimpleMatchVarL Many pat
-    match_code <- matchSimply (Var var) ProcExpr pat env_stk_expr fail_expr
+    match_code <- matchSimply (Var var) (ArrowMatchCtxt ProcExpr) pat env_stk_expr fail_expr
     let pat_ty = hsLPatType pat
     let proc_code = do_premap meth_ids pat_ty env_stk_ty cmd_ty
                     (Lam var match_code)
@@ -755,9 +755,9 @@ dsCmdLam ids local_vars stack_ty res_ty pats body env_ids = do
         in_ty = envStackType env_ids stack_ty
         in_ty' = envStackType env_ids' stack_ty'
 
-    fail_expr <- mkFailExpr LambdaExpr in_ty'
+    fail_expr <- mkFailExpr (ArrowMatchCtxt KappaExpr) in_ty'
     -- match the patterns against the parameters
-    match_code <- matchSimplys (map Var param_ids) LambdaExpr pats core_expr
+    match_code <- matchSimplys (map Var param_ids) (ArrowMatchCtxt KappaExpr) pats core_expr
                     fail_expr
     -- match the parameters against the top of the old stack
     (stack_id, param_code) <- matchVarStack param_ids stack_id' match_code
diff --git a/compiler/GHC/HsToCore/Pmc/Utils.hs b/compiler/GHC/HsToCore/Pmc/Utils.hs
index faced2f27c..c79c1025d6 100644
--- a/compiler/GHC/HsToCore/Pmc/Utils.hs
+++ b/compiler/GHC/HsToCore/Pmc/Utils.hs
@@ -1,4 +1,5 @@
 
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 
 -- | Utility module for the pattern-match coverage checker.
@@ -87,7 +88,7 @@ exhaustiveWarningFlag IfAlt         = Just Opt_WarnIncompletePatterns
 exhaustiveWarningFlag LambdaExpr    = Just Opt_WarnIncompleteUniPatterns
 exhaustiveWarningFlag PatBindRhs    = Just Opt_WarnIncompleteUniPatterns
 exhaustiveWarningFlag PatBindGuards = Just Opt_WarnIncompletePatterns
-exhaustiveWarningFlag ProcExpr      = Just Opt_WarnIncompleteUniPatterns
+exhaustiveWarningFlag (ArrowMatchCtxt c) = arrowMatchContextExhaustiveWarningFlag c
 exhaustiveWarningFlag RecUpd        = Just Opt_WarnIncompletePatternsRecUpd
 exhaustiveWarningFlag ThPatSplice   = Nothing
 exhaustiveWarningFlag PatSyn        = Nothing
@@ -96,6 +97,12 @@ exhaustiveWarningFlag ThPatQuote    = Nothing
 -- etc. They are often *supposed* to be incomplete
 exhaustiveWarningFlag (StmtCtxt {}) = Nothing
 
+arrowMatchContextExhaustiveWarningFlag :: HsArrowMatchContext -> Maybe WarningFlag
+arrowMatchContextExhaustiveWarningFlag = \ case
+  ProcExpr     -> Just Opt_WarnIncompleteUniPatterns
+  ArrowCaseAlt -> Just Opt_WarnIncompletePatterns
+  KappaExpr    -> Just Opt_WarnIncompleteUniPatterns
+
 -- | Check whether any part of pattern match checking is enabled for this
 -- 'HsMatchContext' (does not matter whether it is the redundancy check or the
 -- exhaustiveness check).
diff --git a/compiler/GHC/Rename/Bind.hs b/compiler/GHC/Rename/Bind.hs
index a4c3ab9865..1e4c43cf7d 100644
--- a/compiler/GHC/Rename/Bind.hs
+++ b/compiler/GHC/Rename/Bind.hs
@@ -1220,13 +1220,16 @@ rnMatch' ctxt rnBody (Match { m_ctxt = mf, m_pats = pats, m_grhss = grhss })
 
 emptyCaseErr :: HsMatchContext GhcRn -> TcRnMessage
 emptyCaseErr ctxt = TcRnUnknownMessage $ mkPlainError noHints $
-  hang (text "Empty list of alternatives in" <+> pp_ctxt)
+  hang (text "Empty list of alternatives in" <+> pp_ctxt ctxt)
         2 (text "Use EmptyCase to allow this")
   where
-    pp_ctxt = case ctxt of
-                CaseAlt    -> text "case expression"
-                LambdaExpr -> text "\\case expression"
-                _ -> text "(unexpected)" <+> pprMatchContextNoun ctxt
+    pp_ctxt :: HsMatchContext GhcRn -> SDoc
+    pp_ctxt c = case c of
+      CaseAlt       -> text "case expression"
+      LambdaExpr    -> text "\\case expression"
+      ArrowMatchCtxt ArrowCaseAlt -> text "case expression"
+      ArrowMatchCtxt KappaExpr    -> text "kappa abstraction"
+      _             -> text "(unexpected)" <+> pprMatchContextNoun c
 
 {-
 ************************************************************************
diff --git a/compiler/GHC/Rename/Expr.hs b/compiler/GHC/Rename/Expr.hs
index 93949c5d83..c7ef4dcfbd 100644
--- a/compiler/GHC/Rename/Expr.hs
+++ b/compiler/GHC/Rename/Expr.hs
@@ -553,7 +553,7 @@ rnExpr e@(HsStatic _ expr) = do
 
 rnExpr (HsProc x pat body)
   = newArrowScope $
-    rnPat ProcExpr pat $ \ pat' -> do
+    rnPat (ArrowMatchCtxt ProcExpr) pat $ \ pat' -> do
       { (body',fvBody) <- rnCmdTop body
       ; return (HsProc x pat' body', fvBody) }
 
@@ -798,7 +798,7 @@ rnCmd (HsCmdApp x fun arg)
        ; return (HsCmdApp x fun' arg', fvFun `plusFV` fvArg) }
 
 rnCmd (HsCmdLam _ matches)
-  = do { (matches', fvMatch) <- rnMatchGroup LambdaExpr rnLCmd matches
+  = do { (matches', fvMatch) <- rnMatchGroup (ArrowMatchCtxt KappaExpr) rnLCmd matches
        ; return (HsCmdLam noExtField matches', fvMatch) }
 
 rnCmd (HsCmdPar x lpar e rpar)
@@ -807,12 +807,12 @@ rnCmd (HsCmdPar x lpar e rpar)
 
 rnCmd (HsCmdCase _ expr matches)
   = do { (new_expr, e_fvs) <- rnLExpr expr
-       ; (new_matches, ms_fvs) <- rnMatchGroup CaseAlt rnLCmd matches
+       ; (new_matches, ms_fvs) <- rnMatchGroup (ArrowMatchCtxt ArrowCaseAlt) rnLCmd matches
        ; return (HsCmdCase noExtField new_expr new_matches
                 , e_fvs `plusFV` ms_fvs) }
 
 rnCmd (HsCmdLamCase x matches)
-  = do { (new_matches, ms_fvs) <- rnMatchGroup CaseAlt rnLCmd matches
+  = do { (new_matches, ms_fvs) <- rnMatchGroup (ArrowMatchCtxt ArrowCaseAlt) rnLCmd matches
        ; return (HsCmdLamCase x new_matches, ms_fvs) }
 
 rnCmd (HsCmdIf _ _ p b1 b2)
diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs
index bde384887a..1fa94e496a 100644
--- a/compiler/GHC/Tc/Errors/Ppr.hs
+++ b/compiler/GHC/Tc/Errors/Ppr.hs
@@ -500,7 +500,13 @@ instance Diagnostic TcRnMessage where
     TcRnCannotDeriveInstance cls cls_tys mb_strat newtype_deriving reason
       -> mkSimpleDecorated $
            derivErrDiagnosticMessage cls cls_tys mb_strat newtype_deriving True reason
-
+    TcRnLazyGADTPattern
+      -> mkSimpleDecorated $
+           hang (text "An existential or GADT data constructor cannot be used")
+              2 (text "inside a lazy (~) pattern")
+    TcRnArrowProcGADTPattern
+      -> mkSimpleDecorated $
+           text "Proc patterns cannot use existential or GADT data constructors"
 
   diagnosticReason = \case
     TcRnUnknownMessage m
@@ -711,6 +717,10 @@ instance Diagnostic TcRnMessage where
            DerivErrBadConstructor{}                -> ErrorWithoutFlag
            DerivErrGenerics{}                      -> ErrorWithoutFlag
            DerivErrEnumOrProduct{}                 -> ErrorWithoutFlag
+    TcRnLazyGADTPattern
+      -> ErrorWithoutFlag
+    TcRnArrowProcGADTPattern
+      -> ErrorWithoutFlag
 
   diagnosticHints = \case
     TcRnUnknownMessage m
@@ -915,7 +925,10 @@ instance Diagnostic TcRnMessage where
              -> noHints
     TcRnCannotDeriveInstance cls _ _ newtype_deriving rea
       -> deriveInstanceErrReasonHints cls newtype_deriving rea
-
+    TcRnLazyGADTPattern
+      -> noHints
+    TcRnArrowProcGADTPattern
+      -> noHints
 
 deriveInstanceErrReasonHints :: Class
                              -> UsingGeneralizedNewtypeDeriving
diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs
index a7418e7e58..db0a6b0c33 100644
--- a/compiler/GHC/Tc/Errors/Types.hs
+++ b/compiler/GHC/Tc/Errors/Types.hs
@@ -1373,6 +1373,20 @@ data TcRnMessage where
                            -- an instance for the class.
                            -> TcRnMessage
 
+  {-| TcRnLazyGADTPattern is an error that occurs when a user writes a nested
+      GADT pattern match inside a lazy (~) pattern.
+
+      Test case: gadt/lazypat
+  -}
+  TcRnLazyGADTPattern :: TcRnMessage
+
+  {-| TcRnArrowProcGADTPattern is an error that occurs when a user writes a
+      GADT pattern inside arrow proc notation.
+
+      Test case: arrows/should_fail/arrowfail004.
+  -}
+  TcRnArrowProcGADTPattern :: TcRnMessage
+
 -- | Which parts of a record field are affected by a particular error or warning.
 data RecordFieldPart
   = RecordFieldConstructor !Name
diff --git a/compiler/GHC/Tc/Gen/Arrow.hs b/compiler/GHC/Tc/Gen/Arrow.hs
index 207f83cb51..0d0e482b35 100644
--- a/compiler/GHC/Tc/Gen/Arrow.hs
+++ b/compiler/GHC/Tc/Gen/Arrow.hs
@@ -100,7 +100,7 @@ tcProc pat cmd@(L _ (HsCmdTop names _)) exp_ty
         ; names' <- mapM (tcSyntaxName ProcOrigin arr_ty) names
         ; let cmd_env = CmdEnv { cmd_arr = arr_ty }
         ; (pat', cmd') <- newArrowScope
-                          $ tcCheckPat ProcExpr pat (unrestricted arg_ty)
+                          $ tcCheckPat (ArrowMatchCtxt ProcExpr) pat (unrestricted arg_ty)
                           $ tcCmdTop cmd_env names' cmd (unitTy, res_ty)
         ; let res_co = mkTcTransCo co
                          (mkTcAppCo co1 (mkTcNomReflCo res_ty))
@@ -262,11 +262,13 @@ tc_cmd env
 
                 -- Check the patterns, and the GRHSs inside
         ; (pats', grhss') <- setSrcSpanA mtch_loc                                 $
-                             tcPats LambdaExpr pats (map (unrestricted . mkCheckExpType) arg_tys) $
+                             tcPats (ArrowMatchCtxt KappaExpr)
+                               pats (map (unrestricted . mkCheckExpType) arg_tys) $
                              tc_grhss grhss cmd_stk' (mkCheckExpType res_ty)
 
         ; let match' = L mtch_loc (Match { m_ext = noAnn
-                                         , m_ctxt = LambdaExpr, m_pats = pats'
+                                         , m_ctxt = ArrowMatchCtxt KappaExpr
+                                         , m_pats = pats'
                                          , m_grhss = grhss' })
               arg_tys = map (unrestricted . hsLPatType) pats'
               cmd' = HsCmdLam x (MG { mg_alts = L l [match']
@@ -275,7 +277,7 @@ tc_cmd env
         ; return (mkHsCmdWrap (mkWpCastN co) cmd') }
   where
     n_pats     = length pats
-    match_ctxt = LambdaExpr    -- Maybe KappaExpr?
+    match_ctxt = ArrowMatchCtxt KappaExpr
     pg_ctxt    = PatGuard match_ctxt
 
     tc_grhss (GRHSs x grhss binds) stk_ty res_ty
@@ -350,7 +352,7 @@ tcCmdMatches :: CmdEnv
 tcCmdMatches env scrut_ty matches (stk, res_ty)
   = tcMatchesCase match_ctxt (unrestricted scrut_ty) matches (mkCheckExpType res_ty)
   where
-    match_ctxt = MC { mc_what = CaseAlt,
+    match_ctxt = MC { mc_what = ArrowMatchCtxt ArrowCaseAlt,
                       mc_body = mc_body }
     mc_body body res_ty' = do { res_ty' <- expTypeToType res_ty'
                               ; tcCmd env body (stk, res_ty') }
diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs
index 82d707dd76..78a4e22901 100644
--- a/compiler/GHC/Tc/Gen/Pat.hs
+++ b/compiler/GHC/Tc/Gen/Pat.hs
@@ -1,5 +1,6 @@
 
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TupleSections #-}
 {-# LANGUAGE TypeFamilies #-}
@@ -886,8 +887,10 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty_scaled
           -- Add the stupid theta
         ; setSrcSpanA con_span $ addDataConStupidTheta data_con ctxt_res_tys
 
+        -- Check that this isn't a GADT pattern match
+        -- in situations in which that isn't allowed.
         ; let all_arg_tys = eqSpecPreds eq_spec ++ theta ++ (map scaledThing arg_tys)
-        ; checkExistentials ex_tvs all_arg_tys penv
+        ; checkGADT (RealDataCon data_con) ex_tvs all_arg_tys penv
 
         ; tenv1 <- instTyVarsWith PatOrigin univ_tvs ctxt_res_tys
                   -- NB: Do not use zipTvSubst!  See #14154
@@ -979,8 +982,11 @@ tcPatSynPat penv (L con_span con_name) pat_syn pat_ty arg_pats thing_inside
 
         ; (subst, univ_tvs') <- newMetaTyVars univ_tvs
 
+        -- Check that we aren't matching on a GADT-like pattern synonym
+        -- in situations in which that isn't allowed.
         ; let all_arg_tys = ty : prov_theta ++ (map scaledThing arg_tys)
-        ; checkExistentials ex_tvs all_arg_tys penv
+        ; checkGADT (PatSynCon pat_syn) ex_tvs all_arg_tys penv
+
         ; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX subst ex_tvs
            -- This freshens: Note [Freshen existentials]
 
@@ -1344,11 +1350,15 @@ these bindings scope over 'term'.
 
 The Right Thing is not to confuse these constraints together. But for
 now the Easy Thing is to ensure that we do not have existential or
-GADT constraints in a 'proc', and to short-cut the constraint
-simplification for such vanilla patterns so that it binds no
-constraints. Hence the 'fast path' in tcConPat; but it's also a good
-plan for ordinary vanilla patterns to bypass the constraint
-simplification step.
+GADT constraints in a 'proc', which we do by disallowing any
+non-vanilla pattern match (i.e. one that introduces existential
+variables or provided constraints), in tcDataConPat and tcPatSynPat.
+
+We also short-cut the constraint simplification for such vanilla patterns,
+so that we bind no constraints. Hence the 'fast path' in tcDataConPat;
+which applies more generally (not just within 'proc'), as it's a good
+plan in general to bypass the constraint simplification step entirely
+when it's not needed.
 
 ************************************************************************
 *                                                                      *
@@ -1442,28 +1452,30 @@ maybeWrapPatCtxt pat tcm thing_inside
    msg = hang (text "In the pattern:") 2 (ppr pat)
 
 -----------------------------------------------
-checkExistentials :: [TyVar]   -- existentials
-                  -> [Type]    -- argument types
-                  -> PatEnv -> TcM ()
-    -- See Note [Existential check]]
-    -- See Note [Arrows and patterns]
-checkExistentials ex_tvs tys _
-  | all (not . (`elemVarSet` tyCoVarsOfTypes tys)) ex_tvs = return ()
-checkExistentials _ _ (PE { pe_ctxt = LetPat {}})         = return ()
-checkExistentials _ _ (PE { pe_ctxt = LamPat ProcExpr })  = failWithTc existentialProcPat
-checkExistentials _ _ (PE { pe_lazy = True })             = failWithTc existentialLazyPat
-checkExistentials _ _ _                                   = return ()
-
-existentialLazyPat :: TcRnMessage
-existentialLazyPat
-  = TcRnUnknownMessage $ mkPlainError noHints $
-    hang (text "An existential or GADT data constructor cannot be used")
-       2 (text "inside a lazy (~) pattern")
 
-existentialProcPat :: TcRnMessage
-existentialProcPat
-  = TcRnUnknownMessage $ mkPlainError noHints $
-    text "Proc patterns cannot use existential or GADT data constructors"
+-- | Check that a pattern isn't a GADT, or doesn't have existential variables,
+-- in a situation in which that is not permitted (inside a lazy pattern, or
+-- in arrow notation).
+checkGADT :: ConLike
+          -> [TyVar] -- ^ existentials
+          -> [Type]  -- ^ argument types
+          -> PatEnv
+          -> TcM ()
+checkGADT conlike ex_tvs arg_tys = \case
+  PE { pe_ctxt = LetPat {} }
+    -> return ()
+  PE { pe_ctxt = LamPat (ArrowMatchCtxt {}) }
+    | not $ isVanillaConLike conlike
+    -- See Note [Arrows and patterns]
+    -> failWithTc TcRnArrowProcGADTPattern
+  PE { pe_lazy = True }
+    | has_existentials
+    -- See Note [Existential check]
+    -> failWithTc TcRnLazyGADTPattern
+  _ -> return ()
+  where
+    has_existentials :: Bool
+    has_existentials = any (`elemVarSet` tyCoVarsOfTypes arg_tys) ex_tvs
 
 badFieldCon :: ConLike -> FieldLabelString -> TcRnMessage
 badFieldCon con field
diff --git a/compiler/Language/Haskell/Syntax/Expr.hs b/compiler/Language/Haskell/Syntax/Expr.hs
index 563505e373..2215ed1210 100644
--- a/compiler/Language/Haskell/Syntax/Expr.hs
+++ b/compiler/Language/Haskell/Syntax/Expr.hs
@@ -1674,7 +1674,8 @@ data HsMatchContext p
   | LambdaExpr                  -- ^Patterns of a lambda
   | CaseAlt                     -- ^Patterns and guards on a case alternative
   | IfAlt                       -- ^Guards of a multi-way if alternative
-  | ProcExpr                    -- ^Patterns of a proc
+  | ArrowMatchCtxt              -- ^A pattern match inside arrow notation
+      HsArrowMatchContext
   | PatBindRhs                  -- ^A pattern binding  eg [y] <- e = e
   | PatBindGuards               -- ^Guards of pattern bindings, e.g.,
                                 --    (Just b) | Just _ <- x = e
@@ -1705,6 +1706,12 @@ data HsStmtContext p
   | TransStmtCtxt (HsStmtContext p)  -- ^A branch of a transform stmt
   | ArrowExpr                        -- ^do-notation in an arrow-command context
 
+-- | Haskell arrow match context.
+data HsArrowMatchContext
+  = ProcExpr     -- ^ A proc expression
+  | ArrowCaseAlt -- ^ A case alternative inside arrow notation
+  | KappaExpr    -- ^ An arrow kappa abstraction
+
 data HsDoFlavour
   = DoExpr (Maybe ModuleName)        -- ^[ModuleName.]do { ... }
   | MDoExpr (Maybe ModuleName)       -- ^[ModuleName.]mdo { ... }  ie recursive do-expression
@@ -1767,7 +1774,7 @@ matchSeparator (FunRhs {})   = text "="
 matchSeparator CaseAlt       = text "->"
 matchSeparator IfAlt         = text "->"
 matchSeparator LambdaExpr    = text "->"
-matchSeparator ProcExpr      = text "->"
+matchSeparator (ArrowMatchCtxt{})= text "->"
 matchSeparator PatBindRhs    = text "="
 matchSeparator PatBindGuards = text "="
 matchSeparator (StmtCtxt _)  = text "<-"
@@ -1783,9 +1790,10 @@ pprMatchContext ctxt
   | want_an ctxt = text "an" <+> pprMatchContextNoun ctxt
   | otherwise    = text "a"  <+> pprMatchContextNoun ctxt
   where
-    want_an (FunRhs {}) = True  -- Use "an" in front
-    want_an ProcExpr    = True
-    want_an _           = False
+    want_an (FunRhs {})                = True  -- Use "an" in front
+    want_an (ArrowMatchCtxt ProcExpr)  = True
+    want_an (ArrowMatchCtxt KappaExpr) = True
+    want_an _                          = False
 
 pprMatchContextNoun :: forall p. (Outputable (IdP p), UnXRec p)
                     => HsMatchContext p -> SDoc
@@ -1800,11 +1808,16 @@ pprMatchContextNoun ThPatQuote      = text "Template Haskell pattern quotation"
 pprMatchContextNoun PatBindRhs      = text "pattern binding"
 pprMatchContextNoun PatBindGuards   = text "pattern binding guards"
 pprMatchContextNoun LambdaExpr      = text "lambda abstraction"
-pprMatchContextNoun ProcExpr        = text "arrow abstraction"
+pprMatchContextNoun (ArrowMatchCtxt c)= pprArrowMatchContextNoun c
 pprMatchContextNoun (StmtCtxt ctxt) = text "pattern binding in"
                                       $$ pprAStmtContext ctxt
 pprMatchContextNoun PatSyn          = text "pattern synonym declaration"
 
+pprArrowMatchContextNoun :: HsArrowMatchContext -> SDoc
+pprArrowMatchContextNoun ProcExpr     = text "arrow proc pattern"
+pprArrowMatchContextNoun ArrowCaseAlt = text "case alternative within arrow notation"
+pprArrowMatchContextNoun KappaExpr    = text "arrow kappa abstraction"
+
 -----------------
 pprAStmtContext, pprStmtContext :: (Outputable (IdP p), UnXRec p)
                                 => HsStmtContext p -> SDoc
diff --git a/docs/users_guide/9.2.1-notes.rst b/docs/users_guide/9.2.1-notes.rst
index a80218098e..6a6dec1ed9 100644
--- a/docs/users_guide/9.2.1-notes.rst
+++ b/docs/users_guide/9.2.1-notes.rst
@@ -135,6 +135,21 @@ Language
   will allow the scrutinee to have a multiplicity of ``One``, using its best-effort
   inference algorithm.
 
+* Support for matching on GADT constructors in arrow notation has been removed,
+  as the current implementation of :extension:`Arrows` doesn't handle GADT
+  evidence correctly.
+
+  One possible workaround, for the time being, is to perform GADT matches
+  inside let bindings: ::
+
+      data G a where
+        MkG :: Show a => a -> G a
+
+      foo :: G a -> String
+      foo = proc x -> do
+        let res = case x of { MkG a -> show a }
+        returnA -< res
+
 Compiler
 ~~~~~~~~
 
diff --git a/testsuite/tests/arrows/gadt/ArrowDict.hs b/testsuite/tests/arrows/gadt/ArrowDict.hs
new file mode 100644
index 0000000000..5e8d9e7701
--- /dev/null
+++ b/testsuite/tests/arrows/gadt/ArrowDict.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE Arrows, GADTs #-}
+module ArrowDict where
+
+data D where
+  D :: Show a => a -> D
+
+get :: D -> String
+get = proc (D x) -> do
+  show -< x
diff --git a/testsuite/tests/arrows/gadt/ArrowDict.stderr b/testsuite/tests/arrows/gadt/ArrowDict.stderr
new file mode 100644
index 0000000000..7e18ba340a
--- /dev/null
+++ b/testsuite/tests/arrows/gadt/ArrowDict.stderr
@@ -0,0 +1,6 @@
+
+ArrowDict.hs:8:13: error:
+    • Proc patterns cannot use existential or GADT data constructors
+    • In the pattern: D x
+      In the expression: proc (D x) -> do show -< x
+      In an equation for ‘get’: get = proc (D x) -> do show -< x
diff --git a/testsuite/tests/arrows/should_fail/arrowfail001.hs b/testsuite/tests/arrows/gadt/ArrowExistential.hs
index e106c214aa..e106c214aa 100644
--- a/testsuite/tests/arrows/should_fail/arrowfail001.hs
+++ b/testsuite/tests/arrows/gadt/ArrowExistential.hs
diff --git a/testsuite/tests/arrows/gadt/ArrowExistential.stderr b/testsuite/tests/arrows/gadt/ArrowExistential.stderr
new file mode 100644
index 0000000000..00944f1297
--- /dev/null
+++ b/testsuite/tests/arrows/gadt/ArrowExistential.stderr
@@ -0,0 +1,6 @@
+
+ArrowExistential.hs:16:27: error:
+    • Proc patterns cannot use existential or GADT data constructors
+    • In the pattern: Bar a
+      In a case alternative within arrow notation: Bar a -> foo -< a
+      In the command: case x of Bar a -> foo -< a
diff --git a/testsuite/tests/arrows/gadt/ArrowGADTKappa.hs b/testsuite/tests/arrows/gadt/ArrowGADTKappa.hs
new file mode 100644
index 0000000000..41e342a4eb
--- /dev/null
+++ b/testsuite/tests/arrows/gadt/ArrowGADTKappa.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE Arrows, GADTs #-}
+
+module ShouldFail where
+
+import Control.Arrow
+
+data G where
+  MkG :: Show a => a -> G
+
+handleG :: ( (a, ()) -> b )
+        -> ( (a, (G, ())) -> b )
+        -> ( (a, ()) -> b )
+handleG = undefined
+
+foo :: String -> String
+foo = proc x -> do
+  (id -< x) `handleG` \ (MkG g) -> show -< g
diff --git a/testsuite/tests/arrows/gadt/ArrowGADTKappa.stderr b/testsuite/tests/arrows/gadt/ArrowGADTKappa.stderr
new file mode 100644
index 0000000000..0241dc9739
--- /dev/null
+++ b/testsuite/tests/arrows/gadt/ArrowGADTKappa.stderr
@@ -0,0 +1,6 @@
+
+ArrowGADTKappa.hs:17:26: error:
+    • Proc patterns cannot use existential or GADT data constructors
+    • In the pattern: MkG g
+      In an arrow kappa abstraction: (MkG g) -> show -< g
+      In the command: (id -< x) `handleG` (MkG g) -> show -< g
diff --git a/testsuite/tests/arrows/gadt/ArrowLet1.hs b/testsuite/tests/arrows/gadt/ArrowLet1.hs
new file mode 100644
index 0000000000..d4ba6b182b
--- /dev/null
+++ b/testsuite/tests/arrows/gadt/ArrowLet1.hs
@@ -0,0 +1,11 @@
+
+{-# LANGUAGE Arrows, GADTs #-}
+module ArrowLet1 where
+
+data G a where
+  MkG :: Show a => a -> G a
+
+foo :: G a -> String
+foo = proc x -> do
+  let res = case x of { MkG a -> show a }
+  id -< res
diff --git a/testsuite/tests/arrows/gadt/ArrowLet2.hs b/testsuite/tests/arrows/gadt/ArrowLet2.hs
new file mode 100644
index 0000000000..2dd2c0b2ee
--- /dev/null
+++ b/testsuite/tests/arrows/gadt/ArrowLet2.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE Arrows, GADTs #-}
+module ArrowLet2 where
+
+data D a where
+  D :: D ()
+
+get :: (D a, a) -> ()
+get = proc d -> do
+  let x = case d of { ( D, x ) -> x}
+  id -< x
diff --git a/testsuite/tests/arrows/gadt/ArrowLet3.hs b/testsuite/tests/arrows/gadt/ArrowLet3.hs
new file mode 100644
index 0000000000..5ff3729055
--- /dev/null
+++ b/testsuite/tests/arrows/gadt/ArrowLet3.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE Arrows, GADTs #-}
+module ArrowLet3 where
+
+data A where
+  A :: a -> B a -> A
+data B a where
+  B :: B ()
+
+foo :: A -> ()
+foo = proc a -> do
+  let x = case a of { A x B -> x }
+  id -< x
diff --git a/testsuite/tests/arrows/gadt/ArrowPatSyn1.hs b/testsuite/tests/arrows/gadt/ArrowPatSyn1.hs
new file mode 100644
index 0000000000..3f50402ab6
--- /dev/null
+++ b/testsuite/tests/arrows/gadt/ArrowPatSyn1.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE Arrows, PatternSynonyms #-}
+
+-- #1662
+
+module ArrowPatSyn1 where
+
+import Control.Arrow
+
+data T a where
+  MkT :: Show a => a -> T a
+
+pattern P :: () => Show a => a -> T a
+pattern P a = MkT a
+
+panic :: Arrow arrow => arrow (T a) String
+panic = proc (P x) ->
+  show -< x
diff --git a/testsuite/tests/arrows/gadt/ArrowPatSyn1.stderr b/testsuite/tests/arrows/gadt/ArrowPatSyn1.stderr
new file mode 100644
index 0000000000..5c11f98a3f
--- /dev/null
+++ b/testsuite/tests/arrows/gadt/ArrowPatSyn1.stderr
@@ -0,0 +1,6 @@
+
+ArrowPatSyn1.hs:16:15: error:
+    • Proc patterns cannot use existential or GADT data constructors
+    • In the pattern: P x
+      In the expression: proc (P x) -> show -< x
+      In an equation for ‘panic’: panic = proc (P x) -> show -< x
diff --git a/testsuite/tests/arrows/gadt/ArrowPatSyn2.hs b/testsuite/tests/arrows/gadt/ArrowPatSyn2.hs
new file mode 100644
index 0000000000..bfd4aabe5f
--- /dev/null
+++ b/testsuite/tests/arrows/gadt/ArrowPatSyn2.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE Arrows, PatternSynonyms #-}
+
+-- #1662
+
+module ArrowPatSyn2 where
+
+import Control.Arrow
+
+data T where
+  MkT :: a -> T
+
+pattern P :: () => forall a. () => a -> T
+pattern P a = MkT a
+
+panic :: Arrow arrow => arrow T T
+panic = proc (P x) ->
+  MkT -< x
diff --git a/testsuite/tests/arrows/gadt/ArrowPatSyn2.stderr b/testsuite/tests/arrows/gadt/ArrowPatSyn2.stderr
new file mode 100644
index 0000000000..6274097ded
--- /dev/null
+++ b/testsuite/tests/arrows/gadt/ArrowPatSyn2.stderr
@@ -0,0 +1,6 @@
+
+ArrowPatSyn2.hs:16:15: error:
+    • Proc patterns cannot use existential or GADT data constructors
+    • In the pattern: P x
+      In the expression: proc (P x) -> MkT -< x
+      In an equation for ‘panic’: panic = proc (P x) -> MkT -< x
diff --git a/testsuite/tests/arrows/should_compile/T17423.hs b/testsuite/tests/arrows/gadt/T17423.hs
index 35023f0612..35023f0612 100644
--- a/testsuite/tests/arrows/should_compile/T17423.hs
+++ b/testsuite/tests/arrows/gadt/T17423.hs
diff --git a/testsuite/tests/arrows/gadt/T17423.stderr b/testsuite/tests/arrows/gadt/T17423.stderr
new file mode 100644
index 0000000000..8e8cf00c9d
--- /dev/null
+++ b/testsuite/tests/arrows/gadt/T17423.stderr
@@ -0,0 +1,13 @@
+
+T17423.hs:19:13: error:
+    • Proc patterns cannot use existential or GADT data constructors
+    • In the pattern: DecoBool i c
+      In the expression:
+        proc (DecoBool i c) -> do i1 <- id -< i
+                                  c1 <- id -< c
+                                  returnA -< DecoBool i1 c1
+      In an equation for ‘decoBoolDialog’:
+          decoBoolDialog
+            = proc (DecoBool i c) -> do i1 <- id -< i
+                                        c1 <- id -< c
+                                        ....
diff --git a/testsuite/tests/arrows/gadt/T20469.hs b/testsuite/tests/arrows/gadt/T20469.hs
new file mode 100644
index 0000000000..0e450c06f3
--- /dev/null
+++ b/testsuite/tests/arrows/gadt/T20469.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE Arrows, GADTs #-}
+module T20469 where
+
+data D a where
+  D :: D ()
+
+get :: (D a, a) -> ()
+get = proc (D, x) -> id -< x
diff --git a/testsuite/tests/arrows/gadt/T20469.stderr b/testsuite/tests/arrows/gadt/T20469.stderr
new file mode 100644
index 0000000000..719f43db20
--- /dev/null
+++ b/testsuite/tests/arrows/gadt/T20469.stderr
@@ -0,0 +1,6 @@
+
+T20469.hs:8:13: error:
+    • Proc patterns cannot use existential or GADT data constructors
+    • In the pattern: D
+      In the pattern: (D, x)
+      In the expression: proc (D, x) -> id -< x
diff --git a/testsuite/tests/arrows/gadt/T20470.hs b/testsuite/tests/arrows/gadt/T20470.hs
new file mode 100644
index 0000000000..cb3db52bbc
--- /dev/null
+++ b/testsuite/tests/arrows/gadt/T20470.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE Arrows, GADTs #-}
+module T20470 where
+
+data A where
+  A :: a -> B a -> A
+data B a where
+  B :: B ()
+
+foo :: A -> ()
+foo = proc a ->
+  case a of
+    A x B ->
+      id -< x
diff --git a/testsuite/tests/arrows/gadt/T20470.stderr b/testsuite/tests/arrows/gadt/T20470.stderr
new file mode 100644
index 0000000000..761c7d1446
--- /dev/null
+++ b/testsuite/tests/arrows/gadt/T20470.stderr
@@ -0,0 +1,6 @@
+
+T20470.hs:12:5: error:
+    • Proc patterns cannot use existential or GADT data constructors
+    • In the pattern: A x B
+      In a case alternative within arrow notation: A x B -> id -< x
+      In the command: case a of A x B -> id -< x
diff --git a/testsuite/tests/arrows/should_compile/T5777.hs b/testsuite/tests/arrows/gadt/T5777.hs
index 697473a4a4..f7adb938aa 100644
--- a/testsuite/tests/arrows/should_compile/T5777.hs
+++ b/testsuite/tests/arrows/gadt/T5777.hs
@@ -3,7 +3,8 @@ module T5777 where
 
 import Control.Arrow
 
-data Value a where BoolVal :: Value Bool
+data Value a where
+    BoolVal :: Value Bool
 
 class ArrowInit f where
     arrif :: f b -> ()
diff --git a/testsuite/tests/arrows/gadt/T5777.stderr b/testsuite/tests/arrows/gadt/T5777.stderr
new file mode 100644
index 0000000000..614b829896
--- /dev/null
+++ b/testsuite/tests/arrows/gadt/T5777.stderr
@@ -0,0 +1,6 @@
+
+T5777.hs:13:18: error:
+    • Proc patterns cannot use existential or GADT data constructors
+    • In the pattern: BoolVal
+      In the expression: proc BoolVal -> returnA -< ()
+      In an equation for ‘arrif’: arrif = proc BoolVal -> returnA -< ()
diff --git a/testsuite/tests/arrows/should_compile/T9985.hs b/testsuite/tests/arrows/gadt/T9985.hs
index 243c8d06d9..243c8d06d9 100644
--- a/testsuite/tests/arrows/should_compile/T9985.hs
+++ b/testsuite/tests/arrows/gadt/T9985.hs
diff --git a/testsuite/tests/arrows/gadt/T9985.stderr b/testsuite/tests/arrows/gadt/T9985.stderr
new file mode 100644
index 0000000000..add3f3c67b
--- /dev/null
+++ b/testsuite/tests/arrows/gadt/T9985.stderr
@@ -0,0 +1,6 @@
+
+T9985.hs:29:18: error:
+    • Proc patterns cannot use existential or GADT data constructors
+    • In the pattern: VNil
+      In the pattern: a :> VNil
+      In the expression: proc (a :> VNil) -> returnA -< a
diff --git a/testsuite/tests/arrows/gadt/all.T b/testsuite/tests/arrows/gadt/all.T
new file mode 100644
index 0000000000..e610d15e26
--- /dev/null
+++ b/testsuite/tests/arrows/gadt/all.T
@@ -0,0 +1,32 @@
+
+# These tests all currently fail, as GADTs aren't
+# supported in arrow notation.
+# It would be nice to add proper support, but for the
+# time being we conservatively reject these programs,
+# to avoid Core Lint errors.
+
+test('ArrowDict', normal, compile_fail, [''])
+test('ArrowGADTKappa', normal, compile_fail, [''])
+test('ArrowExistential', normal, compile_fail, [''])
+ # ArrowExistential got an ASSERT error in the stage1 compiler
+ # because we simply are not typechecking arrow commands
+ # correctly.  See #5267, #5609, #5605
+ #
+ # Dec 2014: The fix is patch 'Fix the scope-nesting for arrows'
+ # Oct 2021 update: we currently reject all GADT pattern matches
+ # in arrows, as the implementation just isn't up to it currently.
+
+# Using let-bindings is a workaround for matching on
+# GADTs within arrow notation.
+test('ArrowLet1', normal, compile, [''])
+test('ArrowLet2', normal, compile, [''])
+test('ArrowLet3', normal, compile, [''])
+
+test('ArrowPatSyn1', normal, compile_fail, [''])
+test('ArrowPatSyn2', normal, compile_fail, [''])
+
+test('T5777', normal, compile_fail, [''])
+test('T9985', normal, compile_fail, [''])
+test('T17423', normal, compile_fail, [''])
+test('T20469', normal, compile_fail, [''])
+test('T20470', normal, compile_fail, [''])
diff --git a/testsuite/tests/arrows/should_compile/all.T b/testsuite/tests/arrows/should_compile/all.T
index 4d76dc1648..6d7e1b4102 100644
--- a/testsuite/tests/arrows/should_compile/all.T
+++ b/testsuite/tests/arrows/should_compile/all.T
@@ -16,8 +16,5 @@ test('T5022', normalise_fun(normalise_errmsg), compile, [''])
 test('T5267', expect_broken(5267), compile, [''])
 test('T5283', normal, compile, [''])
 test('T5333', normal, compile, [''])
-test('T5777', normal, compile, [''])
-test('T9985', normal, compile, [''])
-test('T17423', normal, compile, [''])
 test('T18950', normal, compile, [''])
 test('T15175', normal, compile, [''])
diff --git a/testsuite/tests/arrows/should_fail/all.T b/testsuite/tests/arrows/should_fail/all.T
index 4445ecd165..ba8e07440f 100644
--- a/testsuite/tests/arrows/should_fail/all.T
+++ b/testsuite/tests/arrows/should_fail/all.T
@@ -1,12 +1,3 @@
-test('arrowfail001',
-     normal,
-     compile_fail,
-     [''])
- # arrowfail001 got an ASSERT error in the stage1 compiler
- # because we simply are not typechecking arrow commands
- # correctly.  See #5267, #5609, #5605
- # The fix is patch 'Fix the scope-nesting for arrows' Dec 2014
-
 test('arrowfail002', normal, compile_fail, [''])
 test('arrowfail003', normal, compile_fail, [''])
 test('arrowfail004', normal, compile_fail, [''])
diff --git a/testsuite/tests/arrows/should_fail/arrowfail001.stderr b/testsuite/tests/arrows/should_fail/arrowfail001.stderr
deleted file mode 100644
index 7805f80bf5..0000000000
--- a/testsuite/tests/arrows/should_fail/arrowfail001.stderr
+++ /dev/null
@@ -1,6 +0,0 @@
-
-arrowfail001.hs:16:36:
-    No instance for (Foo a) arising from a use of ‘foo’
-    In the expression: foo
-    In the command: foo -< a
-    In a case alternative: Bar a -> foo -< a