Testcase for Coercible and newtype families (#8548)
[ghc.git] / testsuite / tests / typecheck / should_run / TcCoercible.hs
1 {-# LANGUAGE RoleAnnotations, StandaloneDeriving, FlexibleContexts, UndecidableInstances, GADTs, TypeFamilies #-}
2
3 import GHC.Prim (Coercible, coerce)
4 import Data.Monoid (mempty, First(First), Last())
5
6 newtype Age = Age Int deriving Show
7 newtype Foo = Foo Age deriving Show
8 newtype Bar = Bar Age deriving Show
9 newtype Baz = Baz Bar deriving Show
10
11 type role Map nominal representational
12 data Map a b = Map a b deriving Show
13
14 -- Higher kinded coercions (#8541)
15 newtype List a = List [a] deriving Show
16 data T f = T (f Int)
17
18 -- It should be possible to coerce _under_ undersaturated newtypes
19 newtype NonEtad a b = NonEtad (Either b a) deriving Show
20
21 -- It should be possible to coerce recursive newtypes, in some situations
22 -- (#8503)
23 newtype Fix f = Fix (f (Fix f))
24 deriving instance Show (f (Fix f)) => Show (Fix f)
25
26 newtype FixEither a = FixEither (Either a (FixEither a)) deriving Show
27
28 -- This ensures that explicitly given constraints are consulted, even
29 -- at higher depths
30 data Oracle where Oracle :: Coercible (Fix (Either Age)) (Fix (Either Int)) => Oracle
31 foo :: Oracle -> Either Age (Fix (Either Age)) -> Fix (Either Int)
32 foo Oracle = coerce
33
34 -- This ensures that Coercible looks into newtype instances (#8548)
35 data family Fam k
36 newtype instance Fam Int = FamInt Bool deriving Show
37
38 main = do
39 print (coerce $ one :: Age)
40 print (coerce $ age :: Int)
41 print (coerce $ Baz (Bar age) :: Foo)
42
43 print (coerce (id::Bar->Bar) age :: Foo)
44 print (coerce Baz age :: Foo)
45 print (coerce $ (Age 1, Foo age) :: (Baz, Baz))
46
47 print (coerce $ Map one one :: Map Int Age)
48
49 print (coerce $ Just one :: First Int)
50 print (coerce $ (mempty :: Last Age) :: Last Int)
51
52 printT (coerce $ (T (Left age) :: T (Either Age)) :: T (Either Int))
53 printT (coerce $ (T (Left one) :: T (Either Int)) :: T (Either Age))
54 printT (coerce $ (T [one] :: T []) :: T List)
55 printT (coerce $ (T (List [one]) :: T List) :: T [])
56
57 printT (coerce $ (T (NonEtad (Right age)) :: T (NonEtad Age)) :: T (NonEtad Int))
58
59 print (coerce $ (Fix (Left ()) :: Fix (Either ())) :: Either () (Fix (Either ())))
60 print (coerce $ (Left () :: Either () (Fix (Either ()))) :: Fix (Either ()))
61
62 print (coerce $ (FixEither (Left age) :: FixEither Age) :: Either Int (FixEither Int))
63 print (coerce $ (Left one :: Either Int (FixEither Age)) :: FixEither Age)
64
65 print (coerce $ True :: Fam Int)
66 print (coerce $ FamInt True :: Bool)
67
68 foo `seq` return ()
69
70
71 where one = 1 :: Int
72 age = Age one
73 printT (T x) = print x