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.

4 files changed, 76 insertions, 35 deletions

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