diff options
-rw-r--r-- | libraries/base/Data/Type/Coercion.hs | 61 |
1 files changed, 58 insertions, 3 deletions
diff --git a/libraries/base/Data/Type/Coercion.hs b/libraries/base/Data/Type/Coercion.hs index 618d506d64..c40ca5b3c9 100644 --- a/libraries/base/Data/Type/Coercion.hs +++ b/libraries/base/Data/Type/Coercion.hs @@ -97,9 +97,64 @@ instance Coercible a b => Enum (Coercion a b) where -- | @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. +-- | This class contains types where you can learn the coercibility of two +-- types from information contained in /terms/. +-- +-- The result should be @Just Coercion@ if and only if the types applied to @f@ +-- are coercible: +-- +-- @testCoercion (x :: f a) (y :: f b) = Just Coercion@ ⟺ Coercible a b@ +-- +-- === __Guidance on use with singleton types__ +-- +-- It was previously recommend that only singleton types should inhabit this +-- class. However, it is unclear what the singleton types should represent. +-- +-- Normally, a singleton type has one value per *type*: types quotiented by +-- nominal equivalence, i.e. just types. +-- +-- An example of this would be: +-- +-- @ +-- data Nom0 :: Type -> Type where +-- Nom0Int :: Nom0 Int +-- Nom0Bool :: Nom0 Bool +-- @ +-- +-- Which, to make relationship to the next part more clear, let's rewrite more +-- verbosely as: +-- +-- @ +-- data Nom1 :: Type -> Type where +-- Nom1Int :: forall a. a ~ Int => Nom1 a +-- Nom1Bool :: forall a. a ~ Bool => Nom1 a +-- @ +-- +-- But arguably, given that we are testing for coercibility, it would be better +-- to have one value per *representation*: types quotiented by representational +-- equivalence, i.e. equivalence classes of types that are +-- pairwise-'Coercible'. +-- +-- An example of this would be: +-- +-- @ +-- data Rep :: Type -> Type where +-- RepInt :: forall a. a `Coercible` Int => Rep a +-- RepBool :: forall a. a `Coercible` Bool => Rep a +-- @ +-- +-- The goal of this would be to have laws similar to that for 'TestEquality' +-- when used with singletons: +-- +-- @testCoercion (x :: f a) (y :: f b) = Just Refl ⟺ a `Coercible` b ⟺ coerce x = coerce y@ +-- +-- @isJust (testCoercion x y) = coerce x == coerce y@ +-- +-- However, GHC today thinks the argument to 'Rep' must have a nominal role, +-- and therefore the above doesn't work. +-- +-- Regardless, singleton types are not required, however, and so the latter +-- would-be laws are not in fact valid in general. class TestCoercion f where -- | Conditionally prove the representational equality of @a@ and @b@. testCoercion :: f a -> f b -> Maybe (Coercion a b) |