    -- | 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 Hackage.Security.Util.TypedEmbedded
    import Hackage.Security.Util.Pretty

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

    {-------------------------------------------------------------------------------
      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