{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE PolyKinds #-}
module Data.Type.Coercion
( Coercion(..)
, coerceWith
, sym
, trans
, repr
, TestCoercion(..)
) where
import qualified Data.Type.Equality as Eq
import Data.Maybe
import GHC.Enum
import GHC.Show
import GHC.Read
import GHC.Base
data Coercion a b where
Coercion :: Coercible a b => Coercion a b
newtype Sym a b = Sym { unsym :: Coercion b a }
coerceWith :: Coercion a b -> a -> b
coerceWith Coercion x = coerce x
sym :: forall a b. Coercion a b -> Coercion b a
sym Coercion = unsym (coerce (Sym Coercion :: Sym a a))
trans :: Coercion a b -> Coercion b c -> Coercion a c
trans c Coercion = coerce c
repr :: (a Eq.:~: b) -> Coercion a b
repr Eq.Refl = Coercion
deriving instance Eq (Coercion a b)
deriving instance Show (Coercion a b)
deriving instance Ord (Coercion a b)
instance Coercible a b => Read (Coercion a b) where
readsPrec d = readParen (d > 10) (\r -> [(Coercion, s) | ("Coercion",s) <- lex r ])
instance Coercible a b => Enum (Coercion a b) where
toEnum 0 = Coercion
toEnum _ = error "Data.Type.Coercion.toEnum: bad argument"
fromEnum Coercion = 0
instance Coercible a b => Bounded (Coercion a b) where
minBound = Coercion
maxBound = Coercion
class TestCoercion f where
testCoercion :: f a -> f b -> Maybe (Coercion a b)
instance TestCoercion ((Eq.:~:) a) where
testCoercion Eq.Refl Eq.Refl = Just Coercion
instance TestCoercion (Coercion a) where
testCoercion c Coercion = Just $ coerce (sym c)