Split abnf_to_pest and dhall into their own crates

1 files changed, 0 insertions, 616 deletions

diff --git a/src/typecheck.rs b/src/typecheck.rs
deleted file mode 100644
index 62ff7d2..0000000
--- a/src/typecheck.rs
+++ /dev/null
@@ -1,616 +0,0 @@
-#![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"),
-        }
-    }
-}