{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
module Data.Type.Coercion
( Coercion(..)
, coerceWith
, gcoerceWith
, 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
coerceWith :: Coercion a b -> a -> b
coerceWith Coercion x = coerce x
gcoerceWith :: Coercion a b -> (Coercible a b => r) -> r
gcoerceWith Coercion x = x
sym :: Coercion a b -> Coercion b a
sym Coercion = Coercion
trans :: Coercion a b -> Coercion b c -> Coercion a c
trans Coercion Coercion = Coercion
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)
deriving instance Coercible a b => Read (Coercion a b)
instance Coercible a b => Enum (Coercion a b) where
toEnum 0 = Coercion
toEnum _ = errorWithoutStackTrace "Data.Type.Coercion.toEnum: bad argument"
fromEnum Coercion = 0
deriving instance Coercible a b => Bounded (Coercion a b)
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 ((Eq.:~~:) a) where
testCoercion Eq.HRefl Eq.HRefl = Just Coercion
instance TestCoercion (Coercion a) where
testCoercion Coercion Coercion = Just Coercion