Commit 929155fa authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu

Add tests for roles.

Many of the files modified are just wibbles to output, because now
tycons have roles attached to them, which are produced in the debugging
dumps.
parent 5207c0ff
......@@ -9,8 +9,8 @@ T2431.$WRefl [InlPrag=INLINE] :: forall a. a T2431.:~: a
Unf=Unf{Src=InlineStable, TopLvl=True, Arity=0, Value=True,
ConLike=True, WorkFree=True, Expandable=True,
Guidance=ALWAYS_IF(unsat_ok=False,boring_ok=False)
Tmpl= \ (@ a) -> T2431.Refl @ a @ a @~ <a>}]
T2431.$WRefl = \ (@ a) -> T2431.Refl @ a @ a @~ <a>
Tmpl= \ (@ a) -> T2431.Refl @ a @ a @~ <a>_N}]
T2431.$WRefl = \ (@ a) -> T2431.Refl @ a @ a @~ <a>_N
T2431.absurd
:: forall a. (GHC.Types.Int T2431.:~: GHC.Types.Bool) -> a
......
{-# LANGUAGE RoleAnnotations, PolyKinds #-}
module Roles1 where
data T1 a@N = K1 a
data T2 a@R = K2 a
data T3 (a :: k)@P = K3
data T4 (a :: * -> *)@N b = K4 (a b)
data T5 a = K5 a
data T6 a = K6
data T7 a b = K7 b
TYPE SIGNATURES
TYPE CONSTRUCTORS
T1 :: * -> *
data T1 a@N
No C type associated
RecFlag NonRecursive, Promotable
= K1 :: forall a. a -> T1 a Stricts: _
FamilyInstance: none
T2 :: * -> *
data T2 a@R
No C type associated
RecFlag NonRecursive, Promotable
= K2 :: forall a. a -> T2 a Stricts: _
FamilyInstance: none
T3 :: forall (k :: BOX). k -> *
data T3 (k::BOX)@N (a::k)@P
No C type associated
RecFlag NonRecursive, Not promotable
= K3 :: forall (k::BOX) (a::k). T3 k a
FamilyInstance: none
T4 :: (* -> *) -> * -> *
data T4 (a::* -> *)@N b@N
No C type associated
RecFlag NonRecursive, Not promotable
= K4 :: forall (a::* -> *) b. (a b) -> T4 a b Stricts: _
FamilyInstance: none
T5 :: * -> *
data T5 a@R
No C type associated
RecFlag NonRecursive, Promotable
= K5 :: forall a. a -> T5 a Stricts: _
FamilyInstance: none
T6 :: forall (k :: BOX). k -> *
data T6 (k::BOX)@N (a::k)@P
No C type associated
RecFlag NonRecursive, Not promotable
= K6 :: forall (k::BOX) (a::k). T6 k a
FamilyInstance: none
T7 :: forall (k :: BOX). k -> * -> *
data T7 (k::BOX)@N (a::k)@P b@R
No C type associated
RecFlag NonRecursive, Not promotable
= K7 :: forall (k::BOX) (a::k) b. b -> T7 k a b Stricts: _
FamilyInstance: none
COERCION AXIOMS
Dependent modules: []
Dependent packages: [base, ghc-prim, integer-gmp]
==================== Typechecker ====================
{-# LANGUAGE TypeFamilies, GeneralizedNewtypeDeriving,
MultiParamTypeClasses, FunctionalDependencies #-}
-- tests axiom roles
module Roles13 where
newtype Age = MkAge Int
newtype Wrap a = MkWrap a
convert :: Wrap Age -> Int
convert (MkWrap (MkAge i)) = i
==================== Tidy Core ====================
Result size of Tidy Core = {terms: 5, types: 9, coercions: 5}
a :: Roles13.Wrap Roles13.Age -> Roles13.Wrap Roles13.Age
[GblId, Arity=1, Caf=NoCafRefs, Str=DmdType]
a = \ (ds :: Roles13.Wrap Roles13.Age) -> ds
Roles13.convert :: Roles13.Wrap Roles13.Age -> GHC.Types.Int
[GblId, Arity=1, Caf=NoCafRefs, Str=DmdType]
Roles13.convert =
a
`cast` (<Roles13.Wrap Roles13.Age>_R
-> Roles13.NTCo:Wrap[0] Roles13.NTCo:Age[0]
:: (Roles13.Wrap Roles13.Age -> Roles13.Wrap Roles13.Age)
~#
(Roles13.Wrap Roles13.Age -> GHC.Types.Int))
module Roles2 where
import GHC.Ptr
-- these *must* have certain roles, or things break strangely
-- see TcForeign
data T1 a = K1 (IO a)
data T2 a = K2 (FunPtr a)
TYPE SIGNATURES
TYPE CONSTRUCTORS
T1 :: * -> *
data T1 a@R
No C type associated
RecFlag NonRecursive, Not promotable
= K1 :: forall a. (IO a) -> T1 a Stricts: _
FamilyInstance: none
T2 :: * -> *
data T2 a@R
No C type associated
RecFlag NonRecursive, Not promotable
= K2 :: forall a. (FunPtr a) -> T2 a Stricts: _
FamilyInstance: none
COERCION AXIOMS
Dependent modules: []
Dependent packages: [base, ghc-prim, integer-gmp]
==================== Typechecker ====================
{-# LANGUAGE TypeFamilies, MultiParamTypeClasses #-}
module Roles3 where
class C1 a where
meth1 :: a -> a
class C2 a b where
meth2 :: a ~ b => a -> b
class C3 a b where
type F3 b
meth3 :: a -> F3 b -> F3 b
type family F4 a
class C4 a b where
meth4 :: a -> F4 b -> F4 b
type Syn1 a = F4 a
type Syn2 a = [a]
\ No newline at end of file
TYPE SIGNATURES
TYPE CONSTRUCTORS
C1 :: * -> Constraint
class C1 a@R
RecFlag NonRecursive
meth1 :: a -> a
C2 :: * -> * -> Constraint
class C2 a@N b@N
RecFlag NonRecursive
meth2 :: (~) * a b -> a -> b
C3 :: * -> * -> Constraint
class C3 a@R b@N
RecFlag NonRecursive
type family F3 b@N :: *
meth3 :: a -> F3 b -> F3 b
C4 :: * -> * -> Constraint
class C4 a@R b@N
RecFlag NonRecursive
meth4 :: a -> F4 b -> F4 b
F4 :: * -> *
type family F4 a@N :: *
Syn1 :: * -> *
type Syn1 a@N = F4 a
Syn2 :: * -> *
type Syn2 a@R = [a]
COERCION AXIOMS
axiom Roles3.NTCo:C1 :: C1 a = a -> a
axiom Roles3.NTCo:C2 :: C2 a b = a ~ b => a -> b
axiom Roles3.NTCo:C3 :: C3 a b = a -> F3 b -> F3 b
axiom Roles3.NTCo:C4 :: C4 a b = a -> F4 b -> F4 b
Dependent modules: []
Dependent packages: [base, ghc-prim, integer-gmp]
==================== Typechecker ====================
{-# LANGUAGE RoleAnnotations #-}
module Roles4 where
class C1 a@N where
meth1 :: a -> a
class C2 a@R where
meth2 :: a -> a
type Syn1 a@N = [a]
class C3 a where
meth3 :: a -> Syn1 a
TYPE SIGNATURES
TYPE CONSTRUCTORS
C1 :: * -> Constraint
class C1 a@N
RecFlag NonRecursive
meth1 :: a -> a
C2 :: * -> Constraint
class C2 a@R
RecFlag NonRecursive
meth2 :: a -> a
C3 :: * -> Constraint
class C3 a@N
RecFlag NonRecursive
meth3 :: a -> Syn1 a
Syn1 :: * -> *
type Syn1 a@N = [a]
COERCION AXIOMS
axiom Roles4.NTCo:C1 :: C1 a = a -> a
axiom Roles4.NTCo:C2 :: C2 a = a -> a
axiom Roles4.NTCo:C3 :: C3 a = a -> Syn1 a
Dependent modules: []
Dependent packages: [base, ghc-prim, integer-gmp]
==================== Typechecker ====================
......@@ -40,3 +40,9 @@ test('T7704', normal, compile, [''])
test('T7710', normal, compile, [''])
test('AutoDeriveTypeable', normal, compile, [''])
test('Roles1', only_ways('normal'), compile, ['-ddump-tc'])
test('Roles2', only_ways('normal'), compile, ['-ddump-tc'])
test('Roles3', only_ways('normal'), compile, ['-ddump-tc'])
test('Roles4', only_ways('normal'), compile, ['-ddump-tc'])
test('Roles13', only_ways('normal'), compile, ['-ddump-simpl -dsuppress-uniques'])
\ No newline at end of file
......@@ -6,8 +6,11 @@ drvfail016:
$(RM) -f drvfail016.hi-boot drvfail016.o-boot
'$(TEST_HC)' $(TEST_HC_OPTS) -XGeneralizedNewtypeDeriving -c drvfail016.hs-boot; echo $$?
.PHONY: T1133A
.PHONY: T1133A Roles12
T1133A:
'$(TEST_HC)' $(TEST_HC_OPTS) -c T1133A.hs-boot
-'$(TEST_HC)' $(TEST_HC_OPTS) -c T1133A.hs
Roles12:
'$(TEST_HC)' $(TEST_HC_OPTS) -c Roles12.hs-boot
-'$(TEST_HC)' $(TEST_HC_OPTS) -c Roles12.hs
{-# LANGUAGE GeneralizedNewtypeDeriving, TypeFamilies #-}
module Roles10 where
type family F a
type instance F Int = Bool
type instance F Age = Char
class C a where
meth :: a -> F a
instance C Int where
meth = (> 0)
newtype Age = MkAge Int
deriving C
\ No newline at end of file
Roles10.hs:16:12:
Can't make a derived instance of ‛C Age’
(even with cunning newtype deriving):
it is not type-safe to use GeneralizedNewtypeDeriving on this class;
the last parameter of ‛C’ is at role N
In the newtype declaration for ‛Age’
{-# LANGUAGE GADTs, RoleAnnotations #-}
module Roles11 where
data T2 a@R where
K2 :: T2 Int
Roles11.hs:5:1:
Role mismatch on variable a:
Annotation says R but role N is required
In the data declaration for ‛T2’
module Roles12 where
import {-# SOURCE #-} Roles12
data T a
module Roles12 where
data T a
\ No newline at end of file
Roles12.hs:5:6:
Type constructor ‛T’ has conflicting definitions in the module and its hs-boot file
Main module: data T a@P
No C type associated
RecFlag Recursive, Promotable
=
FamilyInstance: none
Boot file: abstract(False) T a@R
No C type associated
RecFlag NonRecursive, Not promotable
FamilyInstance: none
module Roles5 where
data T a@N
class C a@R
type S a@P = Int
\ No newline at end of file
Roles5.hs:3:8:
Illegal role annotation
Perhaps you intended to use -XRoleAnnotations
In the data type declaration for ‛T’
Roles5.hs:4:9:
Illegal role annotation
Perhaps you intended to use -XRoleAnnotations
In the declaration for class C
Roles5.hs:5:8:
Illegal role annotation
Perhaps you intended to use -XRoleAnnotations
In the declaration for type synonym ‛S’
{-# LANGUAGE RoleAnnotations, TypeFamilies #-}
module Roles6 where
type family F a@R
Roles6.hs:5:1:
Illegal role annotation on variable a;
role annotations are not allowed here
In the family declaration for ‛F’
{-# LANGUAGE RoleAnnotations #-}
module Roles7 where
bar :: Int@P -> Int
bar = id
\ No newline at end of file
Roles7.hs:5:8:
Illegal role annotation on Int
In the type signature for ‛bar’
{-# LANGUAGE RoleAnnotations, GADTs #-}
module Roles8 where
data T1 a@P = K1 a
Roles8.hs:5:1:
Role mismatch on variable a:
Annotation says P but role R is required
In the data declaration for ‛T1’
{-# LANGUAGE GeneralizedNewtypeDeriving, RoleAnnotations #-}
module Roles9 where
class C a@N where
meth :: a -> a
instance C Int where
meth = (+ 1)
newtype Age = MkAge Int
deriving C
Roles9.hs:12:12:
Can't make a derived instance of ‛C Age’
(even with cunning newtype deriving):
it is not type-safe to use GeneralizedNewtypeDeriving on this class;
the last parameter of ‛C’ is at role N
In the newtype declaration for ‛Age’
{-# LANGUAGE TypeFamilies, GeneralizedNewtypeDeriving #-}
module T1496 where
data family Z :: * -> *
newtype instance Z Int = ZI Double
newtype instance Z Moo = ZM (Int,Int)
newtype Moo = Moo Int deriving(IsInt)
class IsInt t where
isInt :: c Int -> c t
instance IsInt Int where isInt = id
main = case isInt (ZI 4.0) of ZM tu -> print tu
\ No newline at end of file
T1496.hs:10:32:
Can't make a derived instance of ‛IsInt Moo’
(even with cunning newtype deriving):
it is not type-safe to use GeneralizedNewtypeDeriving on this class;
the last parameter of ‛IsInt’ is at role N
In the newtype declaration for ‛Moo’
......@@ -3,4 +3,6 @@ T2721.hs:15:28:
Can't make a derived instance of ‛C N’
(even with cunning newtype deriving):
the class has associated types
it is not type-safe to use GeneralizedNewtypeDeriving on this class;
the last parameter of ‛C’ is at role N
In the newtype declaration for ‛N’
{-# LANGUAGE RankNTypes, ScopedTypeVariables, StandaloneDeriving, GADTs, GeneralizedNewtypeDeriving, DeriveDataTypeable #-}
module Main where
import Data.Typeable
data Expr a where
Lit :: Typeable a => a -> Expr a
class A a where
mk :: a
class (Typeable a, A a) => B a where
mkExpr :: Expr a
mkExpr = Lit mk
-- dfunAE
instance B a => A (Expr a) where
mk = mkExpr
-- dfunAB
instance A Bool where
mk = True
newtype BOOL = BOOL Bool
deriving (Typeable, A)
instance B Bool
deriving instance B BOOL --dfunBB
showType :: forall a . Expr a -> String
showType (Lit _) = show (typeOf (undefined :: a))
test1 = showType (mk :: Expr BOOL) -- Prints "Bool" (wrong?)
test2 = showType (Lit mk :: Expr BOOL) -- Prints "Main.BOOL" (correct)
main = do { print test1; print test2 }
T4846.hs:29:1:
Can't make a derived instance of ‛B BOOL’
(even with cunning newtype deriving):
it is not type-safe to use GeneralizedNewtypeDeriving on this class;
the last parameter of ‛B’ is at role N
In the stand-alone deriving instance for ‛B BOOL’
{-# LANGUAGE GeneralizedNewtypeDeriving, GADTs #-}
module T7148 where
data SameType a b where
Refl :: SameType a a
coerce :: SameType a b -> a -> b
coerce Refl = id
trans :: SameType a b -> SameType b c -> SameType a c
trans Refl Refl = Refl
sameUnit :: SameType () ()
sameUnit = Refl
class IsoUnit a where
iso1 :: SameType () b -> SameType a b
iso2 :: SameType b () -> SameType b a
instance IsoUnit () where
iso1 = id
iso2 = id
newtype Tagged a b = Tagged b deriving IsoUnit
sameTagged :: SameType (Tagged a b) (Tagged a' b') -> SameType a a'
sameTagged Refl = Refl
unsafe' :: SameType (Tagged a ()) (Tagged a' ())
unsafe' = (iso1 sameUnit) `trans` (iso2 sameUnit)
unsafe :: SameType a b
unsafe = sameTagged unsafe'
--once again inferred type is a -> b
unsafeCoerce = coerce unsafe
\ No newline at end of file
T7148.hs:27:40:
Can't make a derived instance of ‛IsoUnit (Tagged a b)’
(even with cunning newtype deriving):
it is not type-safe to use GeneralizedNewtypeDeriving on this class;
the last parameter of ‛IsoUnit’ is at role N
In the newtype declaration for ‛Tagged’
{-# LANGUAGE TypeFamilies, ScopedTypeVariables,
GeneralizedNewtypeDeriving #-}
module T7148a where
import Control.Monad.ST
data Proxy a = Proxy
type family Result a b
class Convert a where
coerce :: Proxy b -> a -> Result a b
newtype SAFE a = SAFE a
type instance Result (SAFE a) b = a
instance Convert (SAFE a) where
coerce _ (SAFE a) = a
newtype IS_NO_LONGER a = IS_NO_LONGER a deriving Convert
type instance Result (IS_NO_LONGER a) b = b
--infered type is
unsafeCoerce :: forall a b. a -> b
unsafeCoerce = coerce (Proxy :: Proxy b) . IS_NO_LONGER . SAFE
--use it safely
id' :: a -> a
id' = unsafeCoerce
--segfault (with high probability)
crash :: segfault
crash = unsafeCoerce . tail . tail . tail . unsafeCoerce $ True
--time for side effects
unsafePerformIO :: IO a -> a
unsafePerformIO x = runST $ unsafeCoerce x
\ No newline at end of file
T7148a.hs:19:50:
Can't make a derived instance of ‛Convert (IS_NO_LONGER a)’
(even with cunning newtype deriving):
it is not type-safe to use GeneralizedNewtypeDeriving on this class;
the last parameter of ‛Convert’ is at role N
In the newtype declaration for ‛IS_NO_LONGER’
......@@ -41,3 +41,18 @@ test('T1133A',
['$MAKE --no-print-directory -s T1133A'])
test('T5863a', normal, compile_fail, [''])
test('T7959', normal, compile_fail, [''])
test('Roles5', normal, compile_fail, [''])
test('Roles6', normal, compile_fail, [''])
test('Roles7', normal, compile_fail, [''])
test('Roles8', normal, compile_fail, [''])
test('Roles9', normal, compile_fail, [''])
test('Roles10', normal, compile_fail, [''])
test('Roles11', normal, compile_fail, [''])
test('Roles12',
extra_clean(['Roles12.o-boot', 'Roles12.hi-boot']),
run_command, ['$MAKE --no-print-directory -s Roles12'])
test('T1496', normal, compile_fail, [''])
test('T4846', normal, compile_fail, [''])
test('T7148', normal, compile_fail, [''])
test('T7148a', normal, compile_fail, [''])
CasePrune.hs:14:31:
Can't make a derived instance of ‛C A’
(even with cunning newtype deriving):
it is not type-safe to use GeneralizedNewtypeDeriving on this class;
the last parameter of ‛C’ is at role N
In the newtype declaration for ‛A’
......@@ -88,7 +88,7 @@ test('gadt-escape1', normal, compile_fail, [''])
# test('Arith', normal, compile, [''])
test('Session', normal, compile_and_run, [''])
test('CasePrune', normal, compile_and_run, [''])
test('CasePrune', normal, compile_fail, [''])
test('T1999', normal, compile, [''])
test('T1999a', normal, compile, [''])
......
......@@ -3,10 +3,11 @@
module ShouldFail where
-- Wrong return type
data X f = X (f ())
data B a where
B1 :: X []
B2 :: B [Int]
data T1 a where
K1 :: T1 Int
K2 :: T2 Int -> T1 Bool
data T2 a where
L1 :: T2 Int
L2 :: T1 Bool
gadt11.hs:9:3:
Data constructor ‛B1’ returns type ‛X []
instead of an instance of its parent type ‛B a’
In the definition of data constructor ‛B1
In the data declaration for ‛B
gadt11.hs:12:3:
Data constructor ‛L2’ returns type ‛T1 Bool
instead of an instance of its parent type ‛T2 a’
In the definition of data constructor ‛L2
In the data declaration for ‛T2
......@@ -4,12 +4,12 @@ TYPE SIGNATURES
forall c t t1. (Num t, Num t1, Coll c, Elem c ~ (t, t1)) => c -> c
TYPE CONSTRUCTORS
Coll :: * -> Constraint
class Coll c
class Coll c@N
RecFlag NonRecursive
type family Elem c :: *
type family Elem c@N :: *
empty :: c insert :: Elem c -> c -> c
ListColl :: * -> *
data ListColl a
data ListColl a@R
No C type associated
RecFlag NonRecursive, Promotable
= L :: forall a. [a] -> ListColl a Stricts: _
......
......@@ -180,18 +180,20 @@ test('T3064',
[(wordsize(32), 111189536, 10),
# expected value: 56380288 (x86/Linux) (28/6/2011)
# 111189536 (x86/Windows) (30/10/12)
(wordsize(64), 224798696, 5)]),
(wordsize(64), 236404384, 5)]),
# (amd64/Linux) (28/06/2011): 73259544