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.

24 files changed, 314 insertions, 0 deletions

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/gadt/ArrowExistential.hs b/testsuite/tests/arrows/gadt/ArrowExistential.hs
new file mode 100644
index 0000000000..e106c214aa
--- /dev/null
+++ b/testsuite/tests/arrows/gadt/ArrowExistential.hs
@@ -0,0 +1,21 @@
+
+{-# LANGUAGE Arrows, ExistentialQuantification #-}
+
+-- Crashed GHC 6.4 with a lint error
+-- because of the existential
+
+-- Esa Pulkkinen <esa.pulkkinen@kotiposti.net>
+-- Thomas Jäger <ThJaeger@gmail.com>
+
+module ShouldFail where
+
+class Foo a where foo :: a -> ()
+data Bar = forall a. Foo a => Bar a
+
+get :: Bar -> ()
+get = proc x -> case x of Bar a -> foo -< a
+
+-- This should be rejected because the left side of -< (here foo)
+-- should be treated as being outside the scope of the proc: it can't
+-- refer to the local variables x and a (this is enforced), nor the
+-- existentially quantified type variable introduced by unwrapping x.
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/gadt/T17423.hs b/testsuite/tests/arrows/gadt/T17423.hs
new file mode 100644
index 0000000000..35023f0612
--- /dev/null
+++ b/testsuite/tests/arrows/gadt/T17423.hs
@@ -0,0 +1,37 @@
+{-# LANGUAGE Arrows, GADTs #-}
+
+module Main where
+
+import Control.Arrow
+import Control.Category
+import Prelude hiding (id, (.))
+
+data DecoType a where
+   -- | Icons and colours for @False@ and @True@ respectively.
+   DecoBool :: Maybe (String, String) -> Maybe (Int, Int) -> DecoType Bool
+   -- | Icons and colours for ranges within type @a@.
+   DecoRange :: String -> DecoType a
+
+-- Sub-dialog for designing decorated booleans.
+decoBoolDialog :: Gadget (DecoType Bool) (DecoType Bool)
+decoBoolDialog =
+      -- arr (\(DecoBool i c) -> (i, c)) >>> (icons *** colours) >>> arr (uncurry DecoBool)
+      proc (DecoBool i c) -> do   -- Compiler panic in GHC 8.6.5.
+         i1 <- id -< i
+         c1 <- id -< c
+         returnA -< DecoBool i1 c1
+
+
+
+data Gadget b c = Pure (b -> c)
+
+instance Category Gadget where
+   id = Pure id
+   Pure g1 . Pure g2 = Pure $ g1 . g2
+
+instance Arrow Gadget where
+   arr = Pure
+   first (Pure f) = Pure $ \(b, b1) -> (f b, b1)
+
+
+main = putStrLn "Hello world."
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/gadt/T5777.hs b/testsuite/tests/arrows/gadt/T5777.hs
new file mode 100644
index 0000000000..f7adb938aa
--- /dev/null
+++ b/testsuite/tests/arrows/gadt/T5777.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE Arrows, GADTs #-}
+module T5777 where
+
+import Control.Arrow
+
+data Value a where
+    BoolVal :: Value Bool
+
+class ArrowInit f where
+    arrif :: f b -> ()
+
+instance ArrowInit Value where
+    arrif = proc BoolVal -> returnA -< ()
+    -- arrif = arr (\BoolVal -> ())
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/gadt/T9985.hs b/testsuite/tests/arrows/gadt/T9985.hs
new file mode 100644
index 0000000000..243c8d06d9
--- /dev/null
+++ b/testsuite/tests/arrows/gadt/T9985.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE GADTs, ViewPatterns, PatternSynonyms, DataKinds, Arrows, TypeOperators, TypeFamilies, UndecidableInstances, AllowAmbiguousTypes #-}
+module T9985 where
+
+import Control.Arrow
+
+data Nat = Z | S Nat
+data Vec n a where
+  VNil  :: Vec Z a
+  VCons :: a -> Vec n a -> Vec (S n) a
+viewVNil :: Vec Z a -> ()
+viewVNil VNil = ()
+viewVCons :: Vec (S n) a -> (a, Vec n a)
+viewVCons (VCons a as) = (a, as)
+pattern (:>) :: a -> Vec n a -> Vec (S n) a
+pattern a :> as <- (viewVCons -> (a, as))
+pattern VNil' <- (viewVNil -> ())
+
+type family n + m where
+  n + Z   = n
+  n + S m = S (n + m)
+
+type family P2 n where
+  P2 Z     = S Z
+  P2 (S n) = P2 n + P2 n
+
+class A n where
+  a :: Arrow b => b (Vec (P2 n) a) a
+instance A Z where
+  a = proc (a :> VNil) -> returnA -< a
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, [''])