Add test cases for Coercing recursive newtypes (#8503)
authorJoachim Breitner <mail@joachim-breitner.de>
Wed, 20 Nov 2013 10:37:43 +0000 (10:37 +0000)
committerJoachim Breitner <mail@joachim-breitner.de>
Fri, 22 Nov 2013 17:54:12 +0000 (17:54 +0000)
testsuite/tests/typecheck/should_fail/TcCoercibleFail.hs
testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr
testsuite/tests/typecheck/should_run/TcCoercible.hs
testsuite/tests/typecheck/should_run/TcCoercible.stdout

index 082fbad..1ad76d4 100644 (file)
@@ -17,11 +17,20 @@ foo3 = coerce $ Map one () :: Map Age ()
 
 foo4 = coerce $ one :: Down Int
 
-newtype Void a = Void (Void (a,a))
+newtype Void = Void Void
+foo5 = coerce :: Void -> ()
+
+-- Do not test this; fills up memory
+--newtype VoidBad a = VoidBad (VoidBad (a,a))
+--foo5 = coerce :: (VoidBad ()) -> ()
+
+
+-- This shoul fail with a context stack overflow
+newtype Fix f = Fix (f (Fix f))
+foo6 = coerce :: Fix (Either Int) -> Fix (Either Age)
+foo7 = coerce :: Fix (Either Int) -> ()
 
-foo5 = coerce :: (Void ()) -> ()
 
 one :: Int
 one = 1
-
 main = return ()
index 642b1d8..a9af883 100644 (file)
@@ -35,9 +35,25 @@ TcCoercibleFail.hs:18:8:
     In the expression: coerce $ one :: Down Int
     In an equation for ‛foo4’: foo4 = coerce $ one :: Down Int
 
-TcCoercibleFail.hs:22:8:
-    No instance for (Coercible (Void ()) ())
-      because ‛Void’ is a recursive type constuctor
+TcCoercibleFail.hs:21:8:
+    Context reduction stack overflow; size = 21
+    Use -fcontext-stack=N to increase stack size to N
+      Coercible Void ()
+    In the expression: coerce :: Void -> ()
+    In an equation for ‛foo5’: foo5 = coerce :: Void -> ()
+
+TcCoercibleFail.hs:30:8:
+    Context reduction stack overflow; size = 21
+    Use -fcontext-stack=N to increase stack size to N
+      Coercible Int Age
+    In the expression: coerce :: Fix (Either Int) -> Fix (Either Age)
+    In an equation for ‛foo6’:
+        foo6 = coerce :: Fix (Either Int) -> Fix (Either Age)
+
+TcCoercibleFail.hs:31:8:
+    No instance for (Coercible (Either Int (Fix (Either Int))) ())
+      because ‛Either
+                 Int (Fix (Either Int))’ and ‛()’ are different types.
       arising from a use of ‛coerce’
-    In the expression: coerce :: (Void ()) -> ()
-    In an equation for ‛foo5’: foo5 = coerce :: (Void ()) -> ()
+    In the expression: coerce :: Fix (Either Int) -> ()
+    In an equation for ‛foo7’: foo7 = coerce :: Fix (Either Int) -> ()
index 4aa4ac1..855a133 100644 (file)
@@ -1,6 +1,6 @@
-{-# LANGUAGE RoleAnnotations #-}
+{-# LANGUAGE RoleAnnotations, StandaloneDeriving, FlexibleContexts, UndecidableInstances, GADTs #-}
 
-import GHC.Prim (coerce)
+import GHC.Prim (Coercible, coerce)
 import Data.Monoid (mempty, First(First), Last())
 
 newtype Age = Age Int deriving Show
@@ -18,7 +18,18 @@ data T f = T (f Int)
 -- It should be possible to coerce _under_ undersaturated newtypes
 newtype NonEtad a b = NonEtad (Either b a) deriving Show
 
+-- It should be possible to coerce recursive newtypes, in some situations
+-- (#8503)
+newtype Fix f = Fix (f (Fix f))
+deriving instance Show (f (Fix f)) => Show (Fix f)
 
+newtype FixEither a = FixEither (Either a (FixEither a)) deriving Show
+
+-- This ensures that explicitly given constraints are consulted, even 
+-- at higher depths
+data Oracle where Oracle :: Coercible (Fix (Either Age)) (Fix  (Either Int)) => Oracle
+foo :: Oracle -> Either Age (Fix (Either Age)) -> Fix (Either Int)
+foo Oracle = coerce
 
 main = do
     print (coerce $ one                       :: Age)
@@ -41,9 +52,15 @@ main = do
 
     printT (coerce $ (T (NonEtad (Right age)) :: T (NonEtad Age)) :: T (NonEtad Int))
 
-  where one = 1 :: Int
-        age = Age one
-        printT (T x) = print x
+    print (coerce $ (Fix (Left ()) :: Fix (Either ())) :: Either () (Fix (Either ())))
+    print (coerce $ (Left () :: Either () (Fix (Either ()))) :: Fix (Either ()))
 
+    print (coerce $ (FixEither (Left age) :: FixEither Age) :: Either Int (FixEither Int))
+    print (coerce $ (Left one :: Either Int (FixEither Age)) :: FixEither Age)
 
+    foo `seq` return ()
 
+
+  where one = 1 :: Int
+        age = Age one
+        printT (T x) = print x
index 6874804..7e06734 100644 (file)
@@ -12,3 +12,7 @@ Left (Age 1)
 List [1]
 [1]
 NonEtad (Right 1)
+Left ()
+Fix (Left ())
+Left 1
+FixEither (Left (Age 1))