diff options
author | Ben Gamari <ben@smart-cactus.org> | 2019-11-09 09:31:09 -0500 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2019-11-13 07:08:03 -0500 |
commit | 6885e22c83ac34e48a2abdb1958b07904f28eae6 (patch) | |
tree | aa3b62a9f84ed78cf8266b20413941123789dd4e | |
parent | b795637fc74ffb3ac2f37a50f25468a67bf54bc0 (diff) | |
download | haskell-6885e22c83ac34e48a2abdb1958b07904f28eae6.tar.gz |
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.
-rw-r--r-- | testsuite/tests/quantified-constraints/T17458.hs | 40 | ||||
-rw-r--r-- | testsuite/tests/quantified-constraints/T17458.stderr | 18 | ||||
-rw-r--r-- | testsuite/tests/quantified-constraints/all.T | 1 |
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, ['']) |