gistfile1.hs

{-# LANGUAGE GeneralizedNewtypeDeriving, GADTs #-}

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
symm :: SameType a b -> SameType b a
symm Refl = Refl
 
sameUnit :: SameType () ()
sameUnit = Refl

class IsoUnit a where
  iso :: SameType () b -> SameType a b
 
instance IsoUnit () where
  iso = id
  
newtype Tagged a b = Tagged b deriving IsoUnit

sameTagged :: SameType (Tagged a b) (Tagged a' b') -> SameType a a'
sameTagged Refl = Refl
 
part1 :: SameType (Tagged a ()) ()
part1 = iso sameUnit
part2 :: SameType () (Tagged a' ())
part2 = symm part1


unsafe' :: SameType (Tagged a ()) (Tagged a' ())
unsafe' = part1 `trans` part2
 
unsafe :: SameType a b
unsafe = sameTagged unsafe'
 
--once again inferred type is a -> b
unsafeCoerce = coerce unsafe

crash :: Int
crash = unsafeCoerce . tail . tail . tail . unsafeCoerce $ True