Ticket #7148: badUnsafeGADT.hs

File badUnsafeGADT.hs, 793 bytes (added by carter, 20 months ago)

the code for the bugs

Line 
1{-# LANGUAGE GeneralizedNewtypeDeriving, GADTs #-}
2
3data SameType a b where
4  Refl :: SameType a a
5 
6coerce :: SameType a b -> a -> b
7coerce Refl = id
8 
9trans :: SameType a b -> SameType b c -> SameType a c
10trans Refl Refl = Refl
11 
12sameUnit :: SameType () ()
13sameUnit = Refl
14
15
16class IsoUnit a where
17  iso1 :: SameType () b -> SameType a b
18  iso2 :: SameType b () -> SameType b a
19 
20instance IsoUnit () where
21  iso1 = id
22  iso2 = id
23
24
25newtype Tagged a b = Tagged b deriving IsoUnit
26
27sameTagged :: SameType (Tagged a b) (Tagged a' b') -> SameType a a'
28sameTagged Refl = Refl
29 
30unsafe' :: SameType (Tagged a ()) (Tagged a' ())
31unsafe' = (iso1 sameUnit) `trans` (iso2 sameUnit)
32 
33unsafe :: SameType a b
34unsafe = sameTagged unsafe'
35 
36--once again inferred type is a -> b
37unsafeCoerce = coerce unsafe