blob: 1f91286e0526f3fa75190139b854c7d80fc0df10 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
|
{-# 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
|
