Commit 6885e22c authored by Ben Gamari's avatar Ben Gamari 🐢 Committed by Marge Bot

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.
parent b795637f
-- 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!"
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
......@@ -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, [''])
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment