{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE NoImplicitPrelude #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} ----------------------------------------------------------------------------- -- | -- Module : Data.Type.Coercion -- License : BSD-style (see the LICENSE file in the distribution) -- -- Maintainer : libraries@haskell.org -- Stability : experimental -- Portability : not portable -- -- Definition of representational equality ('Coercion'). -- -- @since 4.7.0.0 ----------------------------------------------------------------------------- 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 -- | Representational equality. If @Coercion a b@ is inhabited by some terminating -- value, then the type @a@ has the same underlying representation as the type @b@. -- -- To use this equality in practice, pattern-match on the @Coercion a b@ to get out -- the @Coercible a b@ instance, and then use 'coerce' to apply it. -- -- @since 4.7.0.0 data Coercion a b where Coercion :: Coercible a b => Coercion a b -- with credit to Conal Elliott for 'ty', Erik Hesselink & Martijn van -- Steenbergen for 'type-equality', Edward Kmett for 'eq', and Gabor Greif -- for 'type-eq' -- | Type-safe cast, using representational equality coerceWith :: Coercion a b -> a -> b coerceWith Coercion x = coerce x -- | Generalized form of type-safe cast using representational equality -- -- @since 4.10.0.0 gcoerceWith :: Coercion a b -> (Coercible a b => r) -> r gcoerceWith Coercion x = x -- | Symmetry of representational equality sym :: Coercion a b -> Coercion b a sym Coercion = Coercion -- | Transitivity of representational equality trans :: Coercion a b -> Coercion b c -> Coercion a c trans Coercion Coercion = Coercion -- | Convert propositional (nominal) equality to representational equality 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) -- | @since 4.7.0.0 instance Coercible a b => Read (Coercion a b) where readsPrec d = readParen (d > 10) (\r -> [(Coercion, s) | ("Coercion",s) <- lex r ]) -- | @since 4.7.0.0 instance Coercible a b => Enum (Coercion a b) where toEnum 0 = Coercion toEnum _ = errorWithoutStackTrace "Data.Type.Coercion.toEnum: bad argument" fromEnum Coercion = 0 -- | @since 4.7.0.0 deriving instance Coercible a b => Bounded (Coercion a b) -- | This class contains types where you can learn the equality of two types -- from information contained in /terms/. Typically, only singleton types should -- inhabit this class. class TestCoercion f where -- | Conditionally prove the representational equality of @a@ and @b@. testCoercion :: f a -> f b -> Maybe (Coercion a b) -- | @since 4.7.0.0 instance TestCoercion ((Eq.:~:) a) where testCoercion Eq.Refl Eq.Refl = Just Coercion -- | @since 4.10.0.0 instance TestCoercion ((Eq.:~~:) a) where testCoercion Eq.HRefl Eq.HRefl = Just Coercion -- | @since 4.7.0.0 instance TestCoercion (Coercion a) where testCoercion Coercion Coercion = Just Coercion