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