Commit fd20b873 authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu
parents a3a99eb4 733b6eea
......@@ -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 ====================
......@@ -39,4 +39,10 @@ test('T1133',
test('T7704', normal, compile, [''])
test('T7710', normal, compile, [''])
test('AutoDeriveTypeable', normal, compile, [''])
\ No newline at end of file
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'])