init

[haskell/symantic.git] / Language / Symantic / Expr / Common.hs

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Language.Symantic.Expr.Common where

import Data.Maybe (fromMaybe)
import Data.Proxy (Proxy(..))
import Data.Text (Text)
import Data.Type.Equality ((:~:)(Refl))
import GHC.Prim (Constraint)
import qualified Data.Text as Text

import Language.Symantic.Type

-- * Class 'Expr_from'

-- | Parse given @ast@ into
-- a 'Type_Root_of_Expr' and
-- a 'Forall_Repr_with_Context',
-- or return an 'Error_of_Expr'.
class Expr_from ast (ex:: *) where
        expr_from :: Expr_From ast ex hs ret

-- | Like 'expr_from' but for a root expression.
root_expr_from
 :: forall lam ast root.
 ( Expr_from ast root
 , Root_of_Expr root ~ root )
 => Proxy root -> Proxy lam -> ast
 -> Either (Error_of_Expr ast root)
           (Exists_Type_and_Repr (Type_Root_of_Expr root)
                                 (Forall_Repr root))
root_expr_from _ex _lam ast =
        expr_from (Proxy::Proxy root) ast
         Context_Empty $ \ty (Forall_Repr_with_Context repr) ->
                Right $ Exists_Type_and_Repr ty $
                        Forall_Repr $ repr Context_Empty

-- ** Type 'Expr_From'
type Expr_From ast ex hs ret
 = Proxy ex
 -- ^ Select the 'Expr_from' instance.
 -> ast
 -- ^ The input data to parse.
 -> Context (Lambda_Var (Type_Root_of_Expr ex)) hs
 -- ^ The bound variables in scope and their types:
 -- held in the heterogeneous list @hs@,
 -- from the closest including lambda abstraction to the farest.
 -> ( forall h
    .  Type_Root_of_Expr ex h
    -> Forall_Repr_with_Context ex hs h
    -> Either (Error_of_Expr ast (Root_of_Expr ex)) ret )
 -- ^ The accumulating continuation.
 ->    Either (Error_of_Expr ast (Root_of_Expr ex)) ret

-- | Parse a literal.
lit_from
 :: forall ty lit ex ast hs ret.
 ( ty ~ Type_Root_of_Expr ex
 , Read lit
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast (Root_of_Expr ex))
 ) => (forall repr. Sym_of_Expr ex repr => lit -> repr lit)
 -> ty lit -> Lambda_Var_Name
 -> Expr_From ast ex hs ret
lit_from lit ty_lit toread ex ast _ctx k =
        case read_safe toread of
         Left err -> Left $ error_expr ex $ Error_Expr_Read err ast
         Right (i::lit) -> k ty_lit $ Forall_Repr_with_Context $ const $ lit i

-- | Parse a unary operator.
op1_from
 :: forall root ty lit ex ast hs ret.
 ( ty ~ Type_Root_of_Expr ex
 , root ~ Root_of_Expr ex
 , Eq_Type (Type_Root_of_Expr root)
 , Expr_from ast root
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit)
 -> ty lit -> ast
 -> Expr_From ast ex hs ret
op1_from op ty_lit ast_x ex ast ctx k =
        expr_from (Proxy::Proxy root) ast_x ctx $
         \ty_x (Forall_Repr_with_Context x) ->
        check_eq_type ex ast ty_lit ty_x $ \Refl ->
                k ty_x $ Forall_Repr_with_Context (op . x)

-- | Parse a binary operator.
op2_from
 :: forall root ty lit ex ast hs ret.
 ( ty ~ Type_Root_of_Expr ex
 , root ~ Root_of_Expr ex
 , Eq_Type (Type_Root_of_Expr root)
 , Expr_from ast root
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit -> repr lit)
 -> ty lit -> ast -> ast
 -> Expr_From ast ex hs ret
op2_from op ty_lit ast_x ast_y ex ast ctx k =
        expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Forall_Repr_with_Context x) ->
        expr_from (Proxy::Proxy root) ast_y ctx $ \ty_y (Forall_Repr_with_Context y) ->
        check_eq_type ex ast ty_lit ty_x $ \Refl ->
        check_eq_type ex ast ty_lit ty_y $ \Refl ->
                k ty_x $ Forall_Repr_with_Context $
                 \c -> x c `op` y c

-- ** Type 'Context'

-- | GADT for a typing context,
-- accumulating an @item@ at each lambda;
-- used to accumulate object-types (in 'Expr_from')
-- or host-terms (in 'Repr_Host')
-- associated with the 'Lambda_Var's in scope.
data Context :: (* -> *) -> [*] -> * where
        Context_Empty :: Context item '[]
        Context_Next  :: item h -> Context item hs -> Context item (h ': hs)
infixr 5 `Context_Next`

-- ** Type 'Lambda_Var'
-- | Join a name and a type.
--
-- This data type is used to handle lambda variables by name
-- (instead of DeBruijn indices for instance).
data Lambda_Var ty h
 =   Lambda_Var Lambda_Var_Name (ty h)
type Lambda_Var_Name = Text

-- ** Type 'Forall_Repr_with_Context'
-- | A data type embedding a universal quantification
-- over an interpreter @repr@
-- and qualified by the symantics of an expression.
--
-- Moreover the expression is abstracted by a 'Context'
-- built at parsing time to build a /Higher-Order Abstract Syntax/ (HOAS)
-- for lambda abstractions.
--
-- This data type is used to keep a parsed expression polymorphic enough
-- to stay interpretable by different interpreters.
--
-- NOTE: 'Sym_of_Expr'@ ex repr@
-- is needed to be able to use symantic methods of the parsed expression
-- into a 'Forall_Repr_with_Context'@ ex@.
--
-- NOTE: 'Sym_of_Expr'@ (@'Root_of_Expr'@ ex) repr@
-- is needed to be able to use an expression
-- out of a 'Forall_Repr_with_Context'@ (@'Root_of_Expr'@ ex)@
-- into a 'Forall_Repr_with_Context'@ ex@,
-- which happens when a symantic method includes a polymorphic type
-- and thus calls: 'expr_from'@ (Proxy::Proxy (@'Root_of_Expr'@ ex))@.
data Forall_Repr_with_Context ex hs h
 =   Forall_Repr_with_Context
 (   forall repr. ( Sym_of_Expr ex repr
                  , Sym_of_Expr (Root_of_Expr ex) repr
                  ) => Context repr hs -> repr h )

-- ** Type 'Forall_Repr'
data Forall_Repr ex h
 =   Forall_Repr
 { unForall_Repr :: forall repr
                 .  ( Sym_of_Expr ex repr
                    , Sym_of_Expr (Root_of_Expr ex) repr )
                 => repr h }

-- ** Type family 'Root_of_Expr'
-- | The root expression of an expression.
type family Root_of_Expr (ex:: *) :: *

-- ** Type family 'Sym_of_Expr'
-- | The symantic of an expression.
type family Sym_of_Expr (ex:: *) (repr:: * -> *) :: Constraint

-- ** Type family 'Error_of_Expr'
-- | The error(s) of an expression.
type family Error_of_Expr (ast:: *) (ex:: *) :: *

-- ** Type family 'Type_of_Expr'
-- | The type of an expression, parameterized by a root type.
type family Type_of_Expr (ex:: *) :: {-root-}(* -> *) -> {-h-}* -> *

-- ** Type 'Type_Root_of_Expr'
-- | Convenient alias.
--
-- NOTE: include 'Type_Var' only to use it
-- within 'Error_Expr_Type_mismatch' so far.
type Type_Root_of_Expr (ex:: *)
 =   Type_Root (Type_Var0 :|: Type_Var1 :|: Type_of_Expr (Root_of_Expr ex))

-- * Type 'Expr_Root'
-- | The root expression, passing itself as parameter to the given expression.
newtype Expr_Root (ex:: * -> *)
 =      Expr_Root (ex (Expr_Root ex))
type instance Root_of_Expr (Expr_Root ex) = Expr_Root ex
type instance Type_of_Expr (Expr_Root ex)
 =            Type_of_Expr (ex (Expr_Root ex))
type instance Error_of_Expr ast (Expr_Root ex)
 =            Error_Expr_Alt (Error_Expr (Error_of_Type ast (Type_Root_of_Expr (ex (Expr_Root ex))))
                                         (Type_Root_of_Expr (ex (Expr_Root ex)))
                                         ast)
                             (Error_of_Expr ast (ex (Expr_Root ex)))
type instance Sym_of_Expr (Expr_Root ex) repr
 =            Sym_of_Expr (ex (Expr_Root ex)) repr
instance -- Expr_from
 ( Expr_from ast (ex (Expr_Root ex))
 , Root_of_Expr (ex (Expr_Root ex)) ~ Expr_Root ex
 ) => Expr_from ast (Expr_Root ex) where
        expr_from _ex ctx ast k =
                expr_from (Proxy::Proxy (ex (Expr_Root ex)))
                 ctx ast $ \ty (Forall_Repr_with_Context repr) ->
                        k ty (Forall_Repr_with_Context repr)

{- NOTE: useless code so far.
-- ** Class 'Expr_Root_Lift'
-- | Lift a given expression to a given root expression.
class Expr_Root_Lift ex root where
        expr_root_lift :: ex root -> root
instance
 Lift_Expr ex root =>
 Expr_Root_Lift ex (Expr_Root root) where
        expr_root_lift = Expr_Root . lift_expr
-}

-- * Type 'Expr_Alt'
-- | Expression making an alternative between two expressions.
data Expr_Alt curr next (root:: *)
 =   Expr_Alt_Curr (curr root)
 |   Expr_Alt_Next (next root)
-- | Convenient alias. Requires @TypeOperators@.
--
-- TODO: see if using a type-level list is better.
type (.|.) = Expr_Alt
infixr 5 .|.
type instance Root_of_Expr (Expr_Alt curr next root) = root
type instance Sym_of_Expr (Expr_Alt curr next root) repr
 = ( Sym_of_Expr (curr root) repr
   , Sym_of_Expr (next root) repr
   )
type instance Type_of_Expr (Expr_Alt curr next root)
 = Type_of_Expr_Alt (Type_of_Expr (curr root))
                    (Type_of_Expr (next root))
-- ** Type family 'Type_of_Expr_Alt'
-- | Remove 'No_Type' type when building 'Type_of_Expr'.
type family Type_of_Expr_Alt
 (type_curr:: (* -> *) -> * -> *)
 (type_next:: (* -> *) -> * -> *)
 where
        Type_of_Expr_Alt No_Type next    = next
        Type_of_Expr_Alt curr    No_Type = curr
        Type_of_Expr_Alt curr    next    = Type_Alt curr next

type instance Error_of_Expr ast (Expr_Alt curr next root)
 = Error_of_Expr_Alt ast (Error_of_Expr ast (curr root))
                         (Error_of_Expr ast (next root))
-- ** Type family 'Error_of_Expr_Alt'
-- | Remove 'No_Error_Expr' type when building the error of an expression.
type family Error_of_Expr_Alt ast curr next where
        Error_of_Expr_Alt ast No_Error_Expr next          = next
        Error_of_Expr_Alt ast curr          No_Error_Expr = curr
        Error_of_Expr_Alt ast curr          next          = Error_Expr_Alt curr next

-- ** Type 'No_Error_Expr'
-- | A discarded error.
data No_Error_Expr
 =   No_Error_Expr
 deriving (Eq, Show)

instance -- Expr_from
 ( Expr_from ast (curr root)
 , Expr_from ast (next root)
 , Root_of_Expr (curr root) ~ root
 , Root_of_Expr (next root) ~ root
 , Unlift_Error_Expr (Error_Expr (Error_of_Type ast (Type_Root_of_Expr root))
                                 (Type_Root_of_Expr root) ast)
                     (Error_of_Expr ast root)
 ) => Expr_from ast (Expr_Alt curr next root) where
        expr_from _ex ctx ast k =
                case expr_from (Proxy::Proxy (curr root)) ctx ast $
                 \ty (Forall_Repr_with_Context repr) ->
                        Right $ k ty (Forall_Repr_with_Context repr) of
                 Right ret -> ret
                 Left err ->
                        case unlift_error_expr err of
                         Just (Error_Expr_Unsupported_here _
                          :: Error_Expr (Error_of_Type ast (Type_Root_of_Expr root))
                                        (Type_Root_of_Expr root) ast) ->
                                expr_from (Proxy::Proxy (next root)) ctx ast $
                                 \ty (Forall_Repr_with_Context repr) ->
                                        k ty (Forall_Repr_with_Context repr)
                         _ -> Left err

{- NOTE: useless code so far.
-- ** Type 'Lift_Expr'
-- | Apply 'Peano_of_Expr' on 'Lift_ExprP'.
type Lift_Expr ex exs
 =   Lift_ExprP (Peano_of_Expr ex exs) ex exs

-- | Convenient wrapper around 'expr_liftN',
-- passing it the 'Peano' number from 'Peano_of_Expr'.
lift_expr
 :: forall ex exs (root:: *).
 Lift_Expr ex exs =>
 ex root -> exs root
lift_expr = expr_liftN (Proxy::Proxy (Peano_of_Expr ex exs))

-- *** Type family 'Peano_of_Expr'
-- | Return a 'Peano' number derived from the location
-- of a given expression within a given expression stack,
-- which is used to avoid @OverlappingInstances@.
type family Peano_of_Expr
 (ex::  * -> *)
 (exs:: * -> *) :: * where
        Peano_of_Expr ex    ex                   = Zero
        Peano_of_Expr ex    (Expr_Alt ex   next) = Zero
        Peano_of_Expr other (Expr_Alt curr next) = Succ (Peano_of_Expr other next)

-- *** Class 'Lift_ExprP'
-- | Lift a given expression to the top of a given expression stack including it,
-- by constructing the appropriate sequence of 'Expr_Alt_Curr' and 'Expr_Alt_Next'.
class Lift_ExprP (p:: *) ex exs where
        expr_liftN :: forall (root:: *). Proxy p -> ex root -> exs root
instance Lift_ExprP Zero curr curr where
        expr_liftN _ = id
instance Lift_ExprP Zero curr (Expr_Alt curr next) where
        expr_liftN _ = Expr_Alt_Curr
instance
 Lift_ExprP p other next =>
 Lift_ExprP (Succ p) other (Expr_Alt curr next) where
        expr_liftN _ = Expr_Alt_Next . expr_liftN (Proxy::Proxy p)

-- ** Type 'Unlift_Expr'
-- | Apply 'Peano_of_Expr' on 'Expr_UnliftN'.
type Unlift_Expr ex exs
 =   Expr_UnliftN (Peano_of_Expr ex exs) ex exs

-- | Convenient wrapper around 'expr_unliftN',
-- passing it the 'Peano' number from 'Peano_of_Expr'.
expr_unlift
 :: forall ex exs (root:: *).
 Unlift_Expr ex exs =>
 exs root -> Maybe (ex root)
expr_unlift = expr_unliftN (Proxy::Proxy (Peano_of_Expr ex exs))

-- *** Class 'Expr_UnliftN'
-- | Try to unlift a given expression out of a given expression stack including it,
-- by deconstructing the appropriate sequence of 'Expr_Alt_Curr' and 'Expr_Alt_Next'.
class Expr_UnliftN (p:: *) ex exs where
        expr_unliftN :: forall (root:: *). Proxy p -> exs root -> Maybe (ex root)
instance Expr_UnliftN Zero curr curr where
        expr_unliftN _ = Just
instance Expr_UnliftN Zero curr (Expr_Alt curr next) where
        expr_unliftN _ (Expr_Alt_Curr x) = Just x
        expr_unliftN _ (Expr_Alt_Next _) = Nothing
instance
 Expr_UnliftN p other next =>
 Expr_UnliftN (Succ p) other (Expr_Alt curr next) where
        expr_unliftN _ (Expr_Alt_Next x) = expr_unliftN (Proxy::Proxy p) x
        expr_unliftN _ (Expr_Alt_Curr _) = Nothing
-}

-- ** Type family 'Is_Last_Expr'
-- | Return whether a given expression is the last one in a given expression stack.
--
-- NOTE: each expression parser uses this type family
-- when it encounters unsupported syntax:
-- to know if it is the last expression parser component that will be tried
-- (and thus return 'Error_Expr_Unsupported')
-- or if some other expression parser component shall be tried
-- (and thus return 'Error_Expr_Unsupported_here',
-- which is then handled accordingly by the 'Expr_from' instance of 'Expr_Alt').
type family Is_Last_Expr (ex:: *) (exs:: *) :: Bool where
        Is_Last_Expr ex        ex                        = 'True
        Is_Last_Expr ex        (Expr_Root exs)           = Is_Last_Expr ex (exs (Expr_Root exs))
        Is_Last_Expr (ex root) (Expr_Alt ex   next root) = 'False
        Is_Last_Expr other     (Expr_Alt curr next root) = Is_Last_Expr other (next root)

-- * Type 'Error_Expr_Alt'
-- | Error expression making an alternative between two error expressions.
data Error_Expr_Alt curr next
 =   Error_Expr_Alt_Curr curr
 |   Error_Expr_Alt_Next next
 deriving (Eq, Show)

-- ** Type 'Lift_Error_Expr'
-- | Apply 'Peano_of_Error_Expr' on 'Lift_Error_ExprP'.
type Lift_Error_Expr err errs
 =   Lift_Error_ExprP (Peano_of_Error_Expr err errs) err errs

-- | Convenient wrapper around 'lift_error_exprP',
-- passing it the 'Peano' number from 'Peano_of_Error_Expr'.
lift_error_expr
 :: forall err errs.
 Lift_Error_Expr err errs => err -> errs
lift_error_expr = lift_error_exprP (Proxy::Proxy (Peano_of_Error_Expr err errs))

-- *** Type family 'Peano_of_Error_Expr'
-- | Return a 'Peano' number derived from the location
-- of a given error expression within a given error expression stack,
-- which is used to avoid @OverlappingInstances@.
type family Peano_of_Error_Expr (err:: *) (errs:: *) :: * where
        Peano_of_Error_Expr err   err                        = Zero
        Peano_of_Error_Expr err   (Error_Expr_Alt err  next) = Zero
        Peano_of_Error_Expr other (Error_Expr_Alt curr next) = Succ (Peano_of_Error_Expr other next)

-- *** Class 'Lift_Error_ExprP'
-- | Lift a given expression to the top of a given expression stack including it,
-- by constructing the appropriate sequence of 'Error_Expr_Alt_Curr' and 'Error_Expr_Alt_Next'.
class Lift_Error_ExprP (p:: *) err errs where
        lift_error_exprP :: Proxy p -> err -> errs
instance Lift_Error_ExprP Zero curr curr where
        lift_error_exprP _ = id
instance Lift_Error_ExprP Zero curr (Error_Expr_Alt curr next) where
        lift_error_exprP _ = Error_Expr_Alt_Curr
instance
 Lift_Error_ExprP p other next =>
 Lift_Error_ExprP (Succ p) other (Error_Expr_Alt curr next) where
        lift_error_exprP _ = Error_Expr_Alt_Next . lift_error_exprP (Proxy::Proxy p)

-- ** Type 'Unlift_Error_Expr'
-- | Apply 'Peano_of_Error_Expr' on 'Unlift_Error_ExprP'.
type Unlift_Error_Expr ex exs
 =   Unlift_Error_ExprP (Peano_of_Error_Expr ex exs) ex exs

-- | Convenient wrapper around 'unlift_error_exprP',
-- passing it the 'Peano' number from 'Peano_of_Error_Expr'.
unlift_error_expr
 :: forall ex exs.
 Unlift_Error_Expr ex exs => exs -> Maybe ex
unlift_error_expr = unlift_error_exprP (Proxy::Proxy (Peano_of_Error_Expr ex exs))

-- *** Class 'Unlift_Error_ExprP'
-- | Try to unlift a given expression error out of a given expression error stack including it,
-- by deconstructing the appropriate sequence of 'Error_Expr_Alt_Curr' and 'Error_Expr_Alt_Next'.
class Unlift_Error_ExprP (p:: *) ex exs where
        unlift_error_exprP :: Proxy p -> exs -> Maybe ex
instance Unlift_Error_ExprP Zero curr curr where
        unlift_error_exprP _ = Just
instance Unlift_Error_ExprP Zero curr (Error_Expr_Alt curr next) where
        unlift_error_exprP _ (Error_Expr_Alt_Curr x) = Just x
        unlift_error_exprP _ (Error_Expr_Alt_Next _) = Nothing
instance
 Unlift_Error_ExprP p other next =>
 Unlift_Error_ExprP (Succ p) other (Error_Expr_Alt curr next) where
        unlift_error_exprP _ (Error_Expr_Alt_Next x) = unlift_error_exprP (Proxy::Proxy p) x
        unlift_error_exprP _ (Error_Expr_Alt_Curr _) = Nothing

-- * Type 'Error_Expr_Read'
-- | Common expression errors.
data Error_Expr err_ty ty ast
 =   Error_Expr_Wrong_number_of_arguments ast Int
 -- ^ Wrong number of arguments applied to a term,
 -- the integer is the number of arguments expected.
 |   Error_Expr_Type_mismatch ast (Exists_Type ty) (Exists_Type ty)
 -- ^ Mismatch between respectively expected and actual type.
 |   Error_Expr_Constraint_missing ast {-Exists_Dict-} (Exists_Type ty)
 -- ^ A 'Constraint' is missing.
 |   Error_Expr_Read Error_Read ast
 -- ^ Error when reading a literal.
 |   Error_Expr_Type err_ty ast
 -- ^ Error when parsing a type.
 |   Error_Expr_Unsupported ast
 -- ^ Given syntax is supported by none
 -- of the expression parser components
 -- of the expression stack.
 |   Error_Expr_Unsupported_here ast
 -- ^ Given syntax not supported by
 -- the current expression parser component.
 deriving (Eq, Show)

-- | Convenient type alias.
type Error_Expr_of_Root ast root
 =   Error_Expr (Error_of_Type ast (Type_Root_of_Expr root))
                (Type_Root_of_Expr root)
                ast

-- | Convenient wrapper around 'lift_error_expr',
-- passing the type family boilerplate.
error_expr
 :: forall ast ex ty.
 (ty ~ Type_Root_of_Expr ex)
 => Lift_Error_Expr
   (Error_Expr (Error_of_Type ast ty) ty ast)
   (Error_of_Expr ast (Root_of_Expr ex))
 => Proxy ex
 -> Error_Expr (Error_of_Type ast ty) ty ast
 -> Error_of_Expr ast (Root_of_Expr ex)
error_expr _ = lift_error_expr

-- | Parsing utility to return 'Error_Expr_Unsupported'
-- or 'Error_Expr_Unsupported_here'
-- according to the given expression.
error_expr_unsupported
 :: forall ast ex ty root.
 ( root ~ Root_of_Expr ex
 , ty ~ Type_Root_of_Expr ex
 , Implicit_HBool (Is_Last_Expr ex root)
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 ) => Proxy ex -> ast
 -> Error_of_Expr ast (Root_of_Expr ex)
error_expr_unsupported ex ast =
        case hbool :: HBool (Is_Last_Expr ex root) of
         HTrue  -> error_expr ex $ Error_Expr_Unsupported ast
         HFalse -> error_expr ex $ Error_Expr_Unsupported_here ast

-- | Parsing utility to check that two types are equal,
-- or raise 'Error_Expr_Type_mismatch'.
check_eq_type
 :: forall ast ex root ty x y ret.
 ( root ~ Root_of_Expr ex
 , ty ~ Type_Root_of_Expr ex
 , Eq_Type ty
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 )
 => Proxy ex -> ast -> ty x -> ty y
 -> (x :~: y -> Either (Error_of_Expr ast root) ret)
 -> Either (Error_of_Expr ast root) ret
check_eq_type ex ast x y k =
        case x `eq_type` y of
         Just Refl -> k Refl
         Nothing -> Left $ error_expr ex $
                Error_Expr_Type_mismatch ast
                 (Exists_Type x)
                 (Exists_Type y)
check_eq_type1
 :: forall ast ex root ty h1 h2 a1 a2 ret.
 ( root ~ Root_of_Expr ex
 , ty ~ Type_Root_of_Expr ex
 , Eq_Type1 ty
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 )
 => Proxy ex -> ast -> ty (h1 a1) -> ty (h2 a2)
 -> (h1 :~: h2 -> Either (Error_of_Expr ast root) ret)
 -> Either (Error_of_Expr ast root) ret
check_eq_type1 ex ast h1 h2 k =
        case h1 `eq_type1` h2 of
         Just Refl -> k Refl
         Nothing -> Left $ error_expr ex $
                Error_Expr_Type_mismatch ast
                 (Exists_Type h1)
                 (Exists_Type h2)

-- | Parsing utility to check that a type is has instance of a given 'Constraint',
-- or raise 'Error_Expr_Constraint_missing'.
check_constraint_type
 :: forall ast ex c root ty h ret.
 ( root ~ Root_of_Expr ex
 , ty ~ Type_Root_of_Expr ex
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Constraint_Type c ty
 )
 => Proxy ex -> Proxy c -> ast -> ty h
 -> (Dict (c h) -> Either (Error_of_Expr ast root) ret)
 -> Either (Error_of_Expr ast root) ret
check_constraint_type ex c ast ty k =
        case constraint_type c ty of
         Just Dict -> k Dict
         Nothing -> Left $ error_expr ex $
                Error_Expr_Constraint_missing ast
                 {-(Exists_Dict c)-}
                 -- FIXME: not easy to report the constraint
                 -- and still support 'Eq' and 'Show' deriving.
                 (Exists_Type ty)

-- | Parsing utility to check that a type is has instance of a given 'Constraint'1,
-- or raise 'Error_Expr_Constraint_missing'.
check_constraint1_type
 :: forall ast ex c root ty h a ret.
 ( root ~ Root_of_Expr ex
 , ty ~ Type_Root_of_Expr ex
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Constraint_Type1 c ty
 )
 => Proxy ex -> Proxy c -> ast -> ty (h a)
 -> (Dict (c h) -> Either (Error_of_Expr ast root) ret)
 -> Either (Error_of_Expr ast root) ret
check_constraint1_type ex c ast ty k =
        case constraint_type1 c ty of
         Just Dict -> k Dict
         Nothing -> Left $ error_expr ex $
                Error_Expr_Constraint_missing ast
                 (Exists_Type ty)

-- | Parsing utility to check that the given type is a 'Type_Type1'
-- or raise 'Error_Expr_Type_mismatch'.
check_type1
 :: forall ast ex root ty h ret.
 ( root ~ Root_of_Expr ex
 , ty ~ Type_Root_of_Expr ex
 , Unlift_Type1 (Type_of_Expr root)
 , String_from_Type ty
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 )
 => Proxy ex -> ast -> ty h
 -> (forall (t1:: *).
     ( Type_Type1 t1 ty h
     , Lift_Type1 t1 (Type_Var0 :|: Type_Var1 :|: Type_of_Expr root)
     ) -> Either (Error_of_Expr ast root) ret)
 -> Either (Error_of_Expr ast root) ret
check_type1 ex ast ty k =
        (`fromMaybe` unlift_type1 (unType_Root ty) (Just . k)) $
        Left $
                error_expr ex $
                Error_Expr_Type_mismatch ast
                 (Exists_Type (type_var1 SZero (type_var0 SZero)
                 :: Type_Root_of_Expr ex (Var1 Var0)))
                 (Exists_Type ty)

-- * Type 'Error_Read'
-- | Error parsing a host-term.
data Error_Read
 =   Error_Read Text
 deriving (Eq, Show)

-- | Parse a host-term.
read_safe :: Read h => Text -> Either Error_Read h
read_safe t =
        case reads $ Text.unpack t of
         [(x, "")] -> Right x
         _         -> Left $ Error_Read t