-- | Hiding existentials
module Hackage.Security.Util.Some (
    Some(..)
    -- ** Equality
  , DictEq(..)
  , SomeEq(..)
    -- ** Serialization
  , DictShow(..)
  , SomeShow(..)
    -- ** Pretty-printing
  , DictPretty(..)
  , SomePretty(..)
    -- ** Type checking
  , typecheckSome
  ) where

import Prelude
import Data.Typeable (Typeable)

import Hackage.Security.Util.TypedEmbedded
import Hackage.Security.Util.Pretty

data Some f = forall a. Some (f a)

deriving instance Typeable Some

{-------------------------------------------------------------------------------
  Equality on Some types

  Note that we cannot really do something similar for ordering; what value
  should we return for

  > Some (f x) `compare` Some (f x')

  where @x :: a@, @x' :: a'@ and @a /= a'@? These are incomparable.
-------------------------------------------------------------------------------}

data DictEq a where
  DictEq :: Eq a => DictEq a

-- | Type @f@ satisfies @SomeEq f@ if @f a@ satisfies @Eq@ independent of @a@
class SomeEq f where
  someEq :: DictEq (f a)

instance (Typed f, SomeEq f) => Eq (Some f) where
  Some (f a
x :: f a) == :: Some f -> Some f -> Bool
== Some (f a
y :: f a') =
    case TypeOf f a -> TypeOf f a -> Maybe (a :=: a)
forall typ typ'.
TypeOf f typ -> TypeOf f typ' -> Maybe (typ :=: typ')
forall (f :: * -> *) typ typ'.
Unify f =>
f typ -> f typ' -> Maybe (typ :=: typ')
unify (f a -> TypeOf f a
forall typ. f typ -> TypeOf f typ
forall (f :: * -> *) typ. Typed f => f typ -> TypeOf f typ
typeOf f a
x) (f a -> TypeOf f a
forall typ. f typ -> TypeOf f typ
forall (f :: * -> *) typ. Typed f => f typ -> TypeOf f typ
typeOf f a
y) of
      Maybe (a :=: a)
Nothing   -> Bool
False
      Just a :=: a
Refl -> case DictEq (f a)
forall a. DictEq (f a)
forall (f :: * -> *) a. SomeEq f => DictEq (f a)
someEq :: DictEq (f a) of DictEq (f a)
DictEq -> f a
x f a -> f a -> Bool
forall a. Eq a => a -> a -> Bool
== f a
f a
y

{-------------------------------------------------------------------------------
  Showing Some types
-------------------------------------------------------------------------------}

data DictShow a where
  DictShow :: Show a => DictShow a

-- | Type @f@ satisfies @SomeShow f@ if @f a@ satisfies @Show@ independent of @a@
class SomeShow f where
  someShow :: DictShow (f a)

instance SomeShow f => Show (Some f) where
  show :: Some f -> String
show (Some (f a
x :: f a)) =
    case DictShow (f a)
forall a. DictShow (f a)
forall (f :: * -> *) a. SomeShow f => DictShow (f a)
someShow :: DictShow (f a) of DictShow (f a)
DictShow -> f a -> String
forall a. Show a => a -> String
show f a
x

{-------------------------------------------------------------------------------
  Pretty-printing Some types
-------------------------------------------------------------------------------}

data DictPretty a where
  DictPretty :: Pretty a => DictPretty a

-- | Type @f@ satisfies @SomeShow f@ if @f a@ satisfies @Show@ independent of @a@
class SomePretty f where
  somePretty :: DictPretty (f a)

instance SomePretty f => Pretty (Some f) where
  pretty :: Some f -> String
pretty (Some (f a
x :: f a)) =
    case DictPretty (f a)
forall a. DictPretty (f a)
forall (f :: * -> *) a. SomePretty f => DictPretty (f a)
somePretty :: DictPretty (f a) of DictPretty (f a)
DictPretty -> f a -> String
forall a. Pretty a => a -> String
pretty f a
x

{-------------------------------------------------------------------------------
  Typechecking Some types
-------------------------------------------------------------------------------}

typecheckSome :: Typed f => Some f -> Some (TypeOf f) -> Bool
typecheckSome :: forall (f :: * -> *). Typed f => Some f -> Some (TypeOf f) -> Bool
typecheckSome (Some f a
x) (Some TypeOf f a
typ) =
    case TypeOf f a -> TypeOf f a -> Maybe (a :=: a)
forall typ typ'.
TypeOf f typ -> TypeOf f typ' -> Maybe (typ :=: typ')
forall (f :: * -> *) typ typ'.
Unify f =>
f typ -> f typ' -> Maybe (typ :=: typ')
unify (f a -> TypeOf f a
forall typ. f typ -> TypeOf f typ
forall (f :: * -> *) typ. Typed f => f typ -> TypeOf f typ
typeOf f a
x) TypeOf f a
typ of
      Just a :=: a
Refl -> Bool
True
      Maybe (a :=: a)
Nothing   -> Bool
False