author Joachim Breitner Wed, 20 Nov 2013 10:37:43 +0000 (10:37 +0000) committer Joachim Breitner Fri, 22 Nov 2013 17:54:12 +0000 (17:54 +0000)

@@ -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
+--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