path: root/src/typecheck.rs

#![allow(non_snake_case)]
use std::collections::BTreeMap;
use std::collections::HashSet;
use std::fmt;

use crate::context::Context;
use crate::core;
use crate::core::{Expr, V, X, bx, normalize, shift, subst};
use crate::core::{pi, app};
use crate::core::BuiltinType::*;
use crate::core::BuiltinValue::*;
use crate::core::Const::*;
use crate::core::Expr::*;

use self::TypeMessage::*;

fn axiom<'i, S: Clone>(c: core::Const) -> Result<core::Const, TypeError<'i, S>> {
    match c {
        Type => Ok(Kind),
        Kind => Err(TypeError::new(&Context::new(), &Const(Kind), Untyped)),
    }
}

fn rule(a: core::Const, b: core::Const) -> Result<core::Const, ()> {
    match (a, b) {
        (Type, Kind) => Err(()),
        (Kind, Kind) => Ok(Kind),
        (Type, Type) |
        (Kind, Type) => Ok(Type),
    }
}

fn match_vars(vl: &V, vr: &V, ctx: &[(&str, &str)]) -> bool {
    let xxs = ctx.get(0).map(|x| (x, ctx.split_at(1).1));
    match (vl, vr, xxs) {
        (&V(xL, nL), &V(xR, nR), None) => xL == xR && nL == nR,
        (&V(xL, 0), &V(xR, 0), Some((&(xL2, xR2), _))) if xL == xL2 && xR == xR2 => true,
        (&V(xL, nL), &V(xR, nR), Some((&(xL2, xR2), xs))) => {
            let nL2 = if xL == xL2 { nL - 1 } else { nL };
            let nR2 = if xR == xR2 { nR - 1 } else { nR };
            match_vars(&V(xL, nL2), &V(xR, nR2), xs)
        }
    }
}

fn prop_equal<S, T>(eL0: &Expr<S, X>, eR0: &Expr<T, X>) -> bool
    where S: Clone + ::std::fmt::Debug,
          T: Clone + ::std::fmt::Debug
{
    fn go<'i, S, T>(ctx: &mut Vec<(&'i str, &'i str)>, el: &'i Expr<'i, S, X>, er: &'i Expr<'i, T, X>) -> bool
        where S: Clone + ::std::fmt::Debug,
              T: Clone + ::std::fmt::Debug
    {
        match (el, er) {
            (&Const(Type), &Const(Type)) |
            (&Const(Kind), &Const(Kind)) => true,
            (&Var(ref vL), &Var(ref vR)) => match_vars(vL, vR, &*ctx),
            (&Pi(xL, ref tL, ref bL), &Pi(xR, ref tR, ref bR)) => {
                //ctx <- State.get
                let eq1 = go(ctx, tL, tR);
                if eq1 {
                    //State.put ((xL, xR):ctx)
                    ctx.push((xL, xR));
                    let eq2 = go(ctx, bL, bR);
                    //State.put ctx
                    let _ = ctx.pop();
                    eq2
                } else {
                    false
                }
            }
            (&App(ref fL, ref aL), &App(ref fR, ref aR)) =>
                if go(ctx, fL, fR) { go(ctx, aL, aR) } else { false },
            (&BuiltinType(a), &BuiltinType(b)) => a == b,
            (&Record(ref ktsL0), &Record(ref ktsR0)) => {
                if ktsL0.len() != ktsR0.len() {
                    return false;
                }
                /*
                let go ((kL, tL):ktsL) ((kR, tR):ktsR)
                        | kL == kR = do
                            b <- go tL tR
                            if b
                                then go ktsL ktsR
                                else return False
                    go [] [] = return True
                    go _  _  = return False
                */
                /*
                for ((kL, tL), (kR, tR)) in ktsL0.iter().zip(ktsR0.iter()) {
                    if kL == kR {
                        if !go(ctx, tL, tR) {
                            return false;
                        }
                    } else {
                        return false;
                    }
                }
                true
                */
                !ktsL0.iter().zip(ktsR0.iter()).any(|((kL, tL), (kR, tR))| {
                    kL != kR || !go(ctx, tL, tR)
                })
            }
            (&Union(ref ktsL0), &Union(ref ktsR0)) => {
                if ktsL0.len() != ktsR0.len() {
                    return false;
                }
            /*
                let loop ((kL, tL):ktsL) ((kR, tR):ktsR)
                        | kL == kR = do
                            b <- go tL tR
                            if b
                                then loop ktsL ktsR
                                else return False
                    loop [] [] = return True
                    loop _  _  = return False
                loop (Data.Map.toList ktsL0) (Data.Map.toList ktsR0)
            */
                !ktsL0.iter().zip(ktsR0.iter()).any(|((kL, tL), (kR, tR))| {
                    kL != kR || !go(ctx, tL, tR)
                })
            }
            (_, _) => false,
        }
    }
    let mut ctx = vec![];
    go::<S, T>(&mut ctx, &normalize(eL0), &normalize(eR0))
}

fn op2_type<'i, S, EF>(ctx: &Context<'i, Expr<'i, S, X>>,
                       e: &Expr<'i, S, X>,
                       t: core::BuiltinType,
                       ef: EF,
                       l: &Expr<'i, S, X>,
                       r: &Expr<'i, S, X>)
                       -> Result<Expr<'i, S, X>, TypeError<'i, S>>
    where S: Clone + ::std::fmt::Debug + 'i,
          EF: FnOnce(Expr<'i, S, X>, Expr<'i, S, X>) -> TypeMessage<'i, S>,
{
    let tl = normalize(&type_with(ctx, l)?);
    match tl {
        BuiltinType(lt) if lt == t => {}
        _ => return Err(TypeError::new(ctx, e, ef((*l).clone(), tl))),
    }

    let tr = normalize(&type_with(ctx, r)?);
    match tr {
        BuiltinType(rt) if rt == t => {}
        _ => return Err(TypeError::new(ctx, e, ef((*r).clone(), tr))),
    }

    Ok(BuiltinType(t))
}

/// Type-check an expression and return the expression'i type if type-checking
/// suceeds or an error if type-checking fails
///
/// `type_with` does not necessarily normalize the type since full normalization
/// is not necessary for just type-checking.  If you actually care about the
/// returned type then you may want to `normalize` it afterwards.
pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
                        e: &Expr<'i, S, X>)
                        -> Result<Expr<'i, S, X>, TypeError<'i, S>>
    where S: Clone + ::std::fmt::Debug + 'i
{
    match *e {
        Const(c) => axiom(c).map(Const), //.map(Cow::Owned),
        Var(V(x, n)) => {
            ctx.lookup(x, n)
                .cloned()
                //.map(Cow::Borrowed)
                .ok_or_else(|| TypeError::new(ctx, e, UnboundVariable))
        }
        Lam(x, ref tA, ref b) => {
            let ctx2 = ctx.insert(x, (**tA).clone()).map(|e| core::shift(1, V(x, 0), e));
            let tB = type_with(&ctx2, b)?;
            let p = Pi(x, tA.clone(), bx(tB));
            let _ = type_with(ctx, &p)?;
            //Ok(Cow::Owned(p))
            Ok(p)
        }
        Pi(x, ref tA, ref tB) => {
            let tA2 = normalize::<S, S, X>(&type_with(ctx, tA)?);
            let kA = match tA2 {
                Const(k) => k,
                _        => return Err(TypeError::new(ctx, e, InvalidInputType((**tA).clone()))),
            };

            let ctx2 = ctx.insert(x, (**tA).clone()).map(|e| core::shift(1, V(x, 0), e));
            let tB = normalize(&type_with(&ctx2, tB)?);
            let kB = match tB {
                Const(k) => k,
                _        => return Err(TypeError::new(&ctx2, e, InvalidOutputType(tB))),
            };

            match rule(kA, kB) {
                Err(()) => Err(TypeError::new(ctx, e, NoDependentTypes((**tA).clone(), tB))),
                Ok(k) => Ok(Const(k)),
            }
        }
        App(ref f, ref a) => {
            let tf = normalize(&type_with(ctx, f)?);
            let (x, tA, tB) = match tf {
                Pi(x, tA, tB) => (x, tA, tB),
                _             => return Err(TypeError::new(ctx, e, NotAFunction((**f).clone(), tf))),
            };
            let tA2 = type_with(ctx, a)?;
            if prop_equal(&tA, &tA2) {
                let vx0 = V(x, 0);
                let a2  = shift::<S, S, X>( 1, vx0, a);
                let tB2 = subst(vx0, &a2, &tB);
                let tB3 = shift::<S, S, X>(-1, vx0, &tB2);
                Ok(tB3)
            } else {
                let nf_A  = normalize(&tA);
                let nf_A2 = normalize(&tA2);
                Err(TypeError::new(ctx, e, TypeMismatch((**f).clone(), nf_A, (**a).clone(), nf_A2)))
            }
        }
        Let(f, ref mt, ref r, ref b) => {
            let tR  = type_with(ctx, r)?;
            let ttR = normalize::<S, S, X>(&type_with(ctx, &tR)?);
            let kR  = match ttR {
                Const(k) => k,
                // Don't bother to provide a `let`-specific version of this error
                // message because this should never happen anyway
                _        => return Err(TypeError::new(ctx, e, InvalidInputType(tR))),
            };

            let ctx2 = ctx.insert(f, tR.clone());
            let tB  = type_with(&ctx2, b)?;
            let ttB = normalize::<S, S, X>(&type_with(ctx, &tB)?);
            let kB  = match ttB {
                Const(k) => k,
                // Don't bother to provide a `let`-specific version of this error
                // message because this should never happen anyway
                _        => return Err(TypeError::new(ctx, e, InvalidOutputType(tB))),
            };

            if let Err(()) = rule(kR, kB) {
                return Err(TypeError::new(ctx, e, NoDependentLet(tR, tB)));
            }

            if let Some(ref t) = *mt {
                let nf_t  = normalize(t);
                let nf_tR = normalize(&tR);
                if !prop_equal(&nf_tR, &nf_t) {
                    return Err(TypeError::new(ctx, e, AnnotMismatch((**r).clone(), nf_t, nf_tR)));
                }
            }

            Ok(tB)
        }
        Annot(ref x, ref t) => {
            // This is mainly just to check that `t` is not `Kind`
            let _ = type_with(ctx, t)?;

            let t2 = type_with(ctx, x)?;
            if prop_equal(t, &t2) {
                Ok((**t).clone())
            } else {
                let nf_t  = normalize(t);
                let nf_t2 = normalize(&t2);
                Err(TypeError::new(ctx, e, AnnotMismatch((**x).clone(), nf_t, nf_t2)))
            }
        }
        BuiltinType(t) => Ok(match t {
            List | Optional => pi("_", Const(Type), Const(Type)),
            Bool | Natural | Integer | Double | Text => Const(Type),
        }),
        BoolLit(_) => Ok(BuiltinType(Bool)),
        BoolAnd(ref l, ref r) => op2_type(ctx, e, Bool, CantAnd, l, r),
        BoolOr(ref l, ref r) => op2_type(ctx, e, Bool, CantOr, l, r),
        BoolEQ(ref l, ref r) => op2_type(ctx, e, Bool, CantEQ, l, r),
        BoolNE(ref l, ref r) => op2_type(ctx, e, Bool, CantNE, l, r),
        BoolIf(ref x, ref y, ref z) => {
            let tx = normalize(&type_with(ctx, x)?);
            match tx {
                BuiltinType(Bool) => {}
                _ => return Err(TypeError::new(ctx, e, InvalidPredicate((**x).clone(), tx))),
            }
            let ty = normalize(&type_with(ctx, y)?);
            let tty = normalize(&type_with(ctx, &ty)?);
            match tty {
                Const(Type) => {}
                _ => return Err(TypeError::new(ctx, e, IfBranchMustBeTerm(true, (**y).clone(), ty, tty))),
            }

            let tz = normalize(&type_with(ctx, z)?);
            let ttz = normalize(&type_with(ctx, &tz)?);
            match ttz {
                Const(Type) => {}
                _ => return Err(TypeError::new(ctx, e, IfBranchMustBeTerm(false, (**z).clone(), tz, ttz))),
            }

            if !prop_equal(&ty, &tz) {
                return Err(TypeError::new(ctx, e, IfBranchMismatch((**y).clone(), (**z).clone(), ty, tz)));
            }
            Ok(ty)
        }
        NaturalLit(_) => Ok(BuiltinType(Natural)),
        BuiltinValue(NaturalFold) =>
            Ok(pi("_", Natural,
                pi("natural", Const(Type),
                    pi("succ", pi("_", "natural", "natural"),
                        pi("zero", "natural", "natural"))))),
        BuiltinValue(NaturalBuild) =>
            Ok(pi("_",
                pi("natural", Const(Type),
                    pi("succ", pi("_", "natural", "natural"),
                        pi("zero", "natural", "natural"))),
                Natural)),
        BuiltinValue(NaturalIsZero) |
        BuiltinValue(NaturalEven) |
        BuiltinValue(NaturalOdd) => Ok(pi("_", Natural, Bool)),
        NaturalPlus(ref l, ref r) => op2_type(ctx, e, Natural, CantAdd, l, r),
        NaturalTimes(ref l, ref r) => op2_type(ctx, e, Natural, CantMultiply, l, r),
        IntegerLit(_) => Ok(BuiltinType(Integer)),
        DoubleLit(_) => Ok(BuiltinType(Double)),
        TextLit(_) => Ok(BuiltinType(Text)),
        TextAppend(ref l, ref r) => op2_type(ctx, e, Text, CantTextAppend, l, r),
        ListLit(ref t, ref xs) => {
            let s = normalize::<_, S, _>(&type_with(ctx, t)?);
            match s {
                Const(Type) => {}
                _ => return Err(TypeError::new(ctx, e, InvalidListType((**t).clone()))),
            }
            for (i, x) in xs.iter().enumerate() {
                let t2 = type_with(ctx, x)?;
                if !prop_equal(t, &t2) {
                    let nf_t  = normalize(t);
                    let nf_t2 = normalize(&t2);
                    return Err(TypeError::new(ctx, e, InvalidListElement(i, nf_t, x.clone(), nf_t2)) )
                }
            }
            Ok(App(bx(BuiltinType(List)), t.clone()))
        }
        BuiltinValue(ListBuild) =>
            Ok(pi("a", Const(Type),
                pi("_",
                    pi("list", Const(Type),
                        pi("cons", pi("_", "a", pi("_", "list", "list")),
                            pi("nil", "list", "list"))),
                    app(List, "a")))),
        BuiltinValue(ListFold) =>
            Ok(pi("a", Const(Type),
                pi("_", app(List, "a"),
                    pi("list", Const(Type),
                        pi("cons", pi("_", "a", pi("_", "list", "list")),
                            pi("nil", "list", "list")))))),
        BuiltinValue(ListLength) =>
            Ok(pi("a", Const(Type), pi("_", app(List, "a"), Natural))),
        BuiltinValue(ListHead) |
        BuiltinValue(ListLast) =>
            Ok(pi("a", Const(Type), pi("_", app(List, "a"), app(Optional, "a")))),
        BuiltinValue(ListIndexed) => {
            let mut m = BTreeMap::new();
            m.insert("index", BuiltinType(Natural));
            m.insert("value", Expr::from("a"));
            Ok(pi("a", Const(Type), pi("_", app(List, "a"), app(List, Record(m)))))
        }
        BuiltinValue(ListReverse) =>
            Ok(pi("a", Const(Type), pi("_", app(List, "a"), app(List, "a")))),
        OptionalLit(ref t, ref xs) => {
            let s = normalize::<_, S, _>(&type_with(ctx, t)?);
            match s {
                Const(Type) => {}
                _ => return Err(TypeError::new(ctx, e, InvalidOptionalType((**t).clone()))),
            }
            let n = xs.len();
            if 2 <= n {
                return Err(TypeError::new(ctx, e, InvalidOptionalLiteral(n)));
            }
            for x in xs {
                let t2 = type_with(ctx, x)?;
                if !prop_equal(t, &t2) {
                    let nf_t  = normalize(t);
                    let nf_t2 = normalize(&t2);
                    return Err(TypeError::new(ctx, e, InvalidOptionalElement(nf_t, x.clone(), nf_t2)));
                }
            }
            Ok(App(bx(BuiltinType(Optional)), t.clone()))
        }
        BuiltinValue(OptionalFold) =>
            Ok(pi("a", Const(Type),
                pi("_", app(Optional, "a"),
                    pi("optional", Const(Type),
                        pi("just", pi("_", "a", "optional"),
                            pi("nothing", "optional", "optional")))))),
        Record(ref kts) => {
            for (k, t) in kts {
                let s = normalize::<S, S, X>(&type_with(ctx, t)?);
                match s {
                    Const(Type) => {}
                    _ => return Err(TypeError::new(ctx, e, InvalidFieldType((*k).to_owned(), (*t).clone()))),
                }
            }
            Ok(Const(Type))
        }
        RecordLit(ref kvs) => {
            let kts = kvs.iter().map(|(&k, v)| {
                let t = type_with(ctx, v)?;
                let s = normalize::<S, S, X>(&type_with(ctx, &t)?);
                match s {
                    Const(Type) => {}
                    _ => return Err(TypeError::new(ctx, e, InvalidField((*k).to_owned(), (*v).clone()))),
                }
                Ok((k, t))
            }).collect::<Result<_, _>>()?;
            Ok(Record(kts))
        }
/*
type_with ctx e@(Union     kts   ) = do
    let process (k, t) = do
            s <- fmap Dhall.Core.normalize (type_with ctx t)
            case s of
                Const Type -> return ()
                _          -> Left (TypeError ctx e (InvalidAlternativeType k t))
    mapM_ process (Data.Map.toList kts)
    return (Const Type)
type_with ctx e@(UnionLit k v kts) = do
    case Data.Map.lookup k kts of
        Just _  -> Left (TypeError ctx e (DuplicateAlternative k))
        Nothing -> return ()
    t <- type_with ctx v
    let union = Union (Data.Map.insert k t kts)
    _ <- type_with ctx union
    return union
type_with ctx e@(Combine kvsX kvsY) = do
    tKvsX <- fmap Dhall.Core.normalize (type_with ctx kvsX)
    ktsX  <- case tKvsX of
        Record kts -> return kts
        _          -> Left (TypeError ctx e (MustCombineARecord kvsX tKvsX))

    tKvsY <- fmap Dhall.Core.normalize (type_with ctx kvsY)
    ktsY  <- case tKvsY of
        Record kts -> return kts
        _          -> Left (TypeError ctx e (MustCombineARecord kvsY tKvsY))

    let combineTypes ktsL ktsR = do
            let ks =
                    Data.Set.union (Data.Map.keysSet ktsL) (Data.Map.keysSet ktsR)
            kts <- forM (toList ks) (\k -> do
                case (Data.Map.lookup k ktsL, Data.Map.lookup k ktsR) of
                    (Just (Record ktsL'), Just (Record ktsR')) -> do
                        t <- combineTypes ktsL' ktsR'
                        return (k, t)
                    (Nothing, Just t) -> do
                        return (k, t)
                    (Just t, Nothing) -> do
                        return (k, t)
                    _ -> do
                        Left (TypeError ctx e (FieldCollision k)) )
            return (Record (Data.Map.fromList kts))

    combineTypes ktsX ktsY
type_with ctx e@(Merge kvsX kvsY t) = do
    tKvsX <- fmap Dhall.Core.normalize (type_with ctx kvsX)
    ktsX  <- case tKvsX of
        Record kts -> return kts
        _          -> Left (TypeError ctx e (MustMergeARecord kvsX tKvsX))
    let ksX = Data.Map.keysSet ktsX

    tKvsY <- fmap Dhall.Core.normalize (type_with ctx kvsY)
    ktsY  <- case tKvsY of
        Union kts -> return kts
        _         -> Left (TypeError ctx e (MustMergeUnion kvsY tKvsY))
    let ksY = Data.Map.keysSet ktsY

    let diffX = Data.Set.difference ksX ksY
    let diffY = Data.Set.difference ksY ksX

    if Data.Set.null diffX
        then return ()
        else Left (TypeError ctx e (UnusedHandler diffX))

    let process (kY, tY) = do
            case Data.Map.lookup kY ktsX of
                Nothing  -> Left (TypeError ctx e (MissingHandler diffY))
                Just tX  ->
                    case tX of
                        Pi _ tY' t' -> do
                            if prop_equal tY tY'
                                then return ()
                                else Left (TypeError ctx e (HandlerInputTypeMismatch kY tY tY'))
                            if prop_equal t t'
                                then return ()
                                else Left (TypeError ctx e (HandlerOutputTypeMismatch kY t t'))
                        _ -> Left (TypeError ctx e (HandlerNotAFunction kY tX))
    mapM_ process (Data.Map.toList ktsY)
    return t
    */
        Field(ref r, x) => {
            let t = normalize(&type_with(ctx, r)?);
            match t {
                Record(ref kts) =>
                    kts.get(x).cloned().ok_or_else(|| TypeError::new(ctx, e, MissingField(x.to_owned(), t.clone()))),
                _ => Err(TypeError::new(ctx, e, NotARecord(x.to_owned(), (**r).clone(), t.clone()))),
            }
        }
        /*
type_with ctx   (Note s e'       ) = case type_with ctx e' of
    Left (TypeError ctx2 (Note s' e'') m) -> Left (TypeError ctx2 (Note s' e'') m)
    Left (TypeError ctx2          e''  m) -> Left (TypeError ctx2 (Note s  e'') m)
    Right r                               -> Right r
*/
        Embed(p) => match p {},
        _ => panic!("Unimplemented typecheck case: {:?}", e),
    }
}

/// `typeOf` is the same as `type_with` with an empty context, meaning that the
/// expression must be closed (i.e. no free variables), otherwise type-checking
/// will fail.
pub fn type_of<'i, S: Clone + ::std::fmt::Debug + 'i>(e: &Expr<'i, S, X>) -> Result<Expr<'i, S, X>, TypeError<'i, S>> {
    let ctx = Context::new();
    type_with(&ctx, e) //.map(|e| e.into_owned())
}

/// The specific type error
#[derive(Debug)]
pub enum TypeMessage<'i, S> {
    UnboundVariable,
    InvalidInputType(Expr<'i, S, X>),
    InvalidOutputType(Expr<'i, S, X>),
    NotAFunction(Expr<'i, S, X>, Expr<'i, S, X>),
    TypeMismatch(Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>),
    AnnotMismatch(Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>),
    Untyped,
    InvalidListElement(usize, Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>),
    InvalidListType(Expr<'i, S, X>),
    InvalidOptionalElement(Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>),
    InvalidOptionalLiteral(usize),
    InvalidOptionalType(Expr<'i, S, X>),
    InvalidPredicate(Expr<'i, S, X>, Expr<'i, S, X>),
    IfBranchMismatch(Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>),
    IfBranchMustBeTerm(bool, Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>),
    InvalidField(String, Expr<'i, S, X>),
    InvalidFieldType(String, Expr<'i, S, X>),
    InvalidAlternative(String, Expr<'i, S, X>),
    InvalidAlternativeType(String, Expr<'i, S, X>),
    DuplicateAlternative(String),
    MustCombineARecord(Expr<'i, S, X>, Expr<'i, S, X>),
    FieldCollision(String),
    MustMergeARecord(Expr<'i, S, X>, Expr<'i, S, X>),
    MustMergeUnion(Expr<'i, S, X>, Expr<'i, S, X>),
    UnusedHandler(HashSet<String>),
    MissingHandler(HashSet<String>),
    HandlerInputTypeMismatch(String, Expr<'i, S, X>, Expr<'i, S, X>),
    HandlerOutputTypeMismatch(String, Expr<'i, S, X>, Expr<'i, S, X>),
    HandlerNotAFunction(String, Expr<'i, S, X>),
    NotARecord(String, Expr<'i, S, X>, Expr<'i, S, X>),
    MissingField(String, Expr<'i, S, X>),
    CantAnd(Expr<'i, S, X>, Expr<'i, S, X>),
    CantOr(Expr<'i, S, X>, Expr<'i, S, X>),
    CantEQ(Expr<'i, S, X>, Expr<'i, S, X>),
    CantNE(Expr<'i, S, X>, Expr<'i, S, X>),
    CantTextAppend(Expr<'i, S, X>, Expr<'i, S, X>),
    CantAdd(Expr<'i, S, X>, Expr<'i, S, X>),
    CantMultiply(Expr<'i, S, X>, Expr<'i, S, X>),
    NoDependentLet(Expr<'i, S, X>, Expr<'i, S, X>),
    NoDependentTypes(Expr<'i, S, X>, Expr<'i, S, X>),
}

/// A structured type error that includes context
#[derive(Debug)]
pub struct TypeError<'i, S> {
    pub context: Context<'i, Expr<'i, S, X>>,
    pub current: Expr<'i, S, X>,
    pub type_message: TypeMessage<'i, S>,
}

impl<'i, S: Clone> TypeError<'i, S> {
    pub fn new(context: &Context<'i, Expr<'i, S, X>>,
               current: &Expr<'i, S, X>,
               type_message: TypeMessage<'i, S>)
               -> Self {
        TypeError {
            context: context.clone(),
            current: current.clone(),
            type_message: type_message,
        }
    }
}

impl<'i, S: fmt::Debug> ::std::error::Error for TypeMessage<'i, S> {
    fn description(&self) -> &str {
        match *self {
            UnboundVariable => "Unbound variable",
            InvalidInputType(_) => "Invalid function input",
            InvalidOutputType(_) => "Invalid function output",
            NotAFunction(_, _) => "Not a function",
            TypeMismatch(_, _, _, _) => "Wrong type of function argument",
            _ => "Unhandled error",
        }
    }
}

impl<'i, S> fmt::Display for TypeMessage<'i, S> {
    fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
        match *self {
            UnboundVariable => f.write_str(include_str!("errors/UnboundVariable.txt")),
            TypeMismatch(ref e0, ref e1, ref e2, ref e3) => {
                let template = include_str!("errors/TypeMismatch.txt");
                let s = template
                    .replace("$txt0", &format!("{}", e0))
                    .replace("$txt1", &format!("{}", e1))
                    .replace("$txt2", &format!("{}", e2))
                    .replace("$txt3", &format!("{}", e3));
                f.write_str(&s)
            }
            _ => f.write_str("Unhandled error message"),
        }
    }
}