namespace TermVar: FiTerm
namespace TypeVar: FiType

sort FiTerm
    inh ctx   TermVar
    inh tyctx TypeVar
    | TmVar (x@ctx)
    | TmInt {Int}
    | TmTop
    | TmAbs (t: FiTerm) (ty: FiType) [x: TermVar]
        t.ctx = lhs.ctx, x
    | TmApp (t1: FiTerm) (t2: FiTerm)
    | TmMerge (t1: FiTerm) (t2: FiTerm)
    | TmAnn (t: FiTerm) (ty: FiType)
    | TmRecord (t: FiTerm) {String}
    | TmProj (t: FiTerm) {String}
    | TmAll (ty: FiType) (t: FiTerm) [alpha: TypeVar]
        t.tyctx = lhs.tyctx, alpha
    | TypeApp (t: FiTerm) (ty: FiType)

sort FiType
    inh tyctx TypeVar
    | TyTop
    | TyBot
    | TyInt
    | TyArr (ty1: FiType) (ty2: FiType)
    | TyAnd (ty1: FiType) (ty2: FiType)
    | TyRecord (ty: FiType) {String}
    | TyVar(x@tyctx)
    | TyAll (tyStar: FiType) (ty: FiType) [alpha: TypeVar]
        ty.tyctx = lhs.tyctx, alpha