testsuite: Add test for #17458

As noted in #17458, QuantifiedConstraints and UndecideableInstances
could previously be used to write programs which can loop at runtime.
This was fixed in !1870.

3 files changed, 59 insertions, 0 deletions

diff --git a/testsuite/tests/quantified-constraints/T17458.hs b/testsuite/tests/quantified-constraints/T17458.hs
new file mode 100644
index 0000000000..d19bd2355c
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T17458.hs
@@ -0,0 +1,40 @@
+-- This program is an example of a use of UndecidableInstances and
+-- QuantifiedConstraints which circumvents the usual compile-time solver
+-- termination check and instead produces a program which loops at runtime.
+
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE TypeOperators #-}
+
+import System.IO
+import Data.Void
+import Data.Typeable
+import Data.Type.Equality
+
+class (forall k. k a => k b) => Equ a b
+
+instance Equ a a
+
+data Z' a where
+  Z' :: Z' Void
+
+data Z where
+  Z :: forall a. Equ Void a => Z' a -> Z
+
+checkZ :: Z -> Bool
+checkZ (Z (Z' :: Z' a)) = case eqT of
+  Nothing -> False
+  Just (Refl :: a :~: Void) -> True
+
+main :: IO ()
+main = do
+  hPutStrLn stderr "before..."
+  hPutStrLn stderr $ show $ checkZ $ Z Z'
+  hPutStrLn stderr "after!"
diff --git a/testsuite/tests/quantified-constraints/T17458.stderr b/testsuite/tests/quantified-constraints/T17458.stderr
new file mode 100644
index 0000000000..b8468266dd
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T17458.stderr
@@ -0,0 +1,18 @@
+
+T17458.hs:32:27: error:
+    • Reduction stack overflow; size = 201
+      When simplifying the following type: Typeable Void
+      Use -freduction-depth=0 to disable this check
+      (any upper bound you could choose might fail unpredictably with
+       minor updates to GHC, so disabling the check is recommended if
+       you're sure that type checking should terminate)
+    • In the expression: eqT
+      In the expression:
+        case eqT of
+          Nothing -> False
+          Just (Refl :: a :~: Void) -> True
+      In an equation for ‘checkZ’:
+          checkZ (Z (Z' :: Z' a))
+            = case eqT of
+                Nothing -> False
+                Just (Refl :: a :~: Void) -> True
diff --git a/testsuite/tests/quantified-constraints/all.T b/testsuite/tests/quantified-constraints/all.T
index 6a1d41eeee..ee32339dab 100644
--- a/testsuite/tests/quantified-constraints/all.T
+++ b/testsuite/tests/quantified-constraints/all.T
@@ -27,3 +27,4 @@ test('T17267b', normal, compile_fail, [''])
 test('T17267c', normal, compile_fail, [''])
 test('T17267d', normal, compile_and_run, [''])
 test('T17267e', normal, compile_fail, [''])
+test('T17458', normal, compile_fail, [''])