    -- | Embedded languages with meta level types
    module Hackage.Security.Util.TypedEmbedded (
        (:=:)(Refl)
      , TypeOf
      , Unify(..)
      , Typed(..)
      , AsType(..)
      ) where

    import Prelude
    import Data.Kind (Type)

    -- | Type equality proofs
    --
    -- This is a direct copy of "type-equality:Data.Type.Equality"; if we don't
    -- mind the dependency we can use that package directly.
    data a :=: b where
      Refl :: a :=: a

    type family TypeOf (f :: Type -> Type) :: Type -> Type

    -- | Equality check that gives us a type-level equality proof.
    class Unify f where
      unify :: f typ -> f typ' -> Maybe (typ :=: typ')

    -- | Embedded languages with type inference
    class Unify (TypeOf f) => Typed f where
      typeOf :: f typ -> TypeOf f typ

    -- | Cast from one type to another
    --
    -- By default (for language with type inference) we just compare the types
    -- returned by 'typeOf'; however, in languages in which terms can have more
    -- than one type this may not be the correct definition (indeed, for such
    -- languages we cannot give an instance of 'Typed').
    class AsType f where
      asType :: f typ -> TypeOf f typ' -> Maybe (f typ')
      default asType :: Typed f => f typ -> TypeOf f typ' -> Maybe (f typ')
      asType f typ
    x TypeOf f typ'
    typ = case TypeOf f typ -> TypeOf f typ' -> Maybe (typ :=: typ')
    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 typ -> TypeOf f typ
    forall typ. f typ -> TypeOf f typ
    forall (f :: * -> *) typ. Typed f => f typ -> TypeOf f typ
    typeOf f typ
    x) TypeOf f typ'
    typ of
                       Just typ :=: typ'
    Refl -> f typ' -> Maybe (f typ')
    forall a. a -> Maybe a
    Just f typ
    f typ'
    x
                       Maybe (typ :=: typ')
    Nothing   -> Maybe (f typ')
    forall a. Maybe a
    Nothing