rustfmt

10 files changed, 658 insertions, 349 deletions

diff --git a/abnf_to_pest/src/lib.rs b/abnf_to_pest/src/lib.rs
index 7381113..38347ed 100644
--- a/abnf_to_pest/src/lib.rs
+++ b/abnf_to_pest/src/lib.rs
@@ -1,5 +1,5 @@
-use std::collections::HashMap;
 use itertools::Itertools;
+use std::collections::HashMap;
 
 pub struct PestRuleSettings {
     pub visible: bool,
@@ -8,14 +8,23 @@ pub struct PestRuleSettings {
 
 impl Default for PestRuleSettings {
     fn default() -> Self {
-        PestRuleSettings { visible: true, replace: None }
+        PestRuleSettings {
+            visible: true,
+            replace: None,
+        }
     }
 }
 
-pub fn abnf_to_pest(data: &Vec<u8>, rule_settings: &HashMap<String, PestRuleSettings>) -> std::io::Result<String> {
+pub fn abnf_to_pest(
+    data: &Vec<u8>,
+    rule_settings: &HashMap<String, PestRuleSettings>,
+) -> std::io::Result<String> {
     use abnf::abnf::*;
-    use pretty::{Doc, BoxDoc};
-    fn format_rule(x: Rule, rule_settings: &HashMap<String, PestRuleSettings>) -> Doc<BoxDoc<()>> {
+    use pretty::{BoxDoc, Doc};
+    fn format_rule(
+        x: Rule,
+        rule_settings: &HashMap<String, PestRuleSettings>,
+    ) -> Doc<BoxDoc<()>> {
         let rulename = format_rulename(x.name);
         let default = Default::default();
         let setting = rule_settings.get(&rulename).unwrap_or(&default);
@@ -36,7 +45,13 @@ pub fn abnf_to_pest(data: &Vec<u8>, rule_settings: &HashMap<String, PestRuleSett
     }
     fn format_rulename(x: String) -> String {
         let x = x.replace("-", "_");
-        if x == "if" || x == "else" || x == "as" || x == "let" || x == "in" || x == "fn" {
+        if x == "if"
+            || x == "else"
+            || x == "as"
+            || x == "let"
+            || x == "in"
+            || x == "fn"
+        {
             x + "_"
         } else {
             x
@@ -44,19 +59,27 @@ pub fn abnf_to_pest(data: &Vec<u8>, rule_settings: &HashMap<String, PestRuleSett
     }
     fn format_alternation(x: Alternation) -> Doc<'static, BoxDoc<'static, ()>> {
         Doc::intersperse(
-            x.concatenations.into_iter().map(|x| format_concatenation(x).nest(2).group()),
-            Doc::space().append(Doc::text("| "))
+            x.concatenations
+                .into_iter()
+                .map(|x| format_concatenation(x).nest(2).group()),
+            Doc::space().append(Doc::text("| ")),
         )
     }
-    fn format_concatenation(x: Concatenation) -> Doc<'static, BoxDoc<'static, ()>> {
+    fn format_concatenation(
+        x: Concatenation,
+    ) -> Doc<'static, BoxDoc<'static, ()>> {
         Doc::intersperse(
             x.repetitions.into_iter().map(format_repetition),
-            Doc::space().append(Doc::text("~ "))
+            Doc::space().append(Doc::text("~ ")),
         )
     }
     fn format_repetition(x: Repetition) -> Doc<'static, BoxDoc<'static, ()>> {
-        format_element(x.element)
-            .append(x.repeat.map(format_repeat).map(Doc::text).unwrap_or(Doc::nil()))
+        format_element(x.element).append(
+            x.repeat
+                .map(format_repeat)
+                .map(Doc::text)
+                .unwrap_or(Doc::nil()),
+        )
     }
     fn format_repeat(x: Repeat) -> String {
         match (x.min.unwrap_or(0), x.max) {
@@ -72,15 +95,16 @@ pub fn abnf_to_pest(data: &Vec<u8>, rule_settings: &HashMap<String, PestRuleSett
         use abnf::abnf::Element::*;
         match x {
             Rulename(s) => Doc::text(format_rulename(s)),
-            Group(g) =>
-                Doc::text("(")
-                    .append(format_alternation(g.alternation).nest(4).group())
-                    .append(Doc::text(")")),
-            Option(o) =>
-                Doc::text("(")
-                    .append(format_alternation(o.alternation).nest(4).group())
-                    .append(Doc::text(")?")),
-            CharVal(s) => Doc::text(format!("^\"{}\"", s.replace("\"", "\\\"").replace("\\", "\\\\"))),
+            Group(g) => Doc::text("(")
+                .append(format_alternation(g.alternation).nest(4).group())
+                .append(Doc::text(")")),
+            Option(o) => Doc::text("(")
+                .append(format_alternation(o.alternation).nest(4).group())
+                .append(Doc::text(")?")),
+            CharVal(s) => Doc::text(format!(
+                "^\"{}\"",
+                s.replace("\"", "\\\"").replace("\\", "\\\\")
+            )),
             NumVal(r) => Doc::text(format_range(r)),
             ProseVal(_) => unimplemented!(),
         }
@@ -88,8 +112,12 @@ pub fn abnf_to_pest(data: &Vec<u8>, rule_settings: &HashMap<String, PestRuleSett
     fn format_range(x: Range) -> String {
         use abnf::abnf::Range::*;
         match x {
-            Range(x, y) => format!("'{}'..'{}'", format_char(x), format_char(y)),
-            OneOf(v) => format!("\"{}\"", v.into_iter().map(format_char).join("")),
+            Range(x, y) => {
+                format!("'{}'..'{}'", format_char(x), format_char(y))
+            }
+            OneOf(v) => {
+                format!("\"{}\"", v.into_iter().map(format_char).join(""))
+            }
         }
     }
     fn format_char(x: u64) -> String {
@@ -104,11 +132,12 @@ pub fn abnf_to_pest(data: &Vec<u8>, rule_settings: &HashMap<String, PestRuleSett
         }
         format!("\\u{{{:02X}}}", x)
     }
-    let make_err = |e| std::io::Error::new(std::io::ErrorKind::Other, format!("{}", e));
+    let make_err =
+        |e| std::io::Error::new(std::io::ErrorKind::Other, format!("{}", e));
 
     let rules = rulelist_comp(&data).map_err(make_err)?.1;
-    let formatted_rules = rules.into_iter().map(|x| format_rule(x, rule_settings));
+    let formatted_rules =
+        rules.into_iter().map(|x| format_rule(x, rule_settings));
     let doc: Doc<_> = Doc::intersperse(formatted_rules, Doc::newline());
     Ok(format!("{}", doc.pretty(80)))
 }
-
diff --git a/dhall/src/context.rs b/dhall/src/context.rs
index c2e1913..b88a677 100644
--- a/dhall/src/context.rs
+++ b/dhall/src/context.rs
@@ -34,7 +34,12 @@ impl<'i, T> Context<'i, T> {
     }
 
     pub fn map<U, F: Fn(&T) -> U>(&self, f: F) -> Context<'i, U> {
-        Context(self.0.iter().map(|(k, v)| (*k, v.iter().map(&f).collect())).collect())
+        Context(
+            self.0
+                .iter()
+                .map(|(k, v)| (*k, v.iter().map(&f).collect()))
+                .collect(),
+        )
     }
 }
 
diff --git a/dhall/src/core.rs b/dhall/src/core.rs
index a0e686d..340cb04 100644
--- a/dhall/src/core.rs
+++ b/dhall/src/core.rs
@@ -1078,8 +1078,10 @@ where
                 }
                 (App(box Builtin(OptionalBuild), a0), g) => {
                     let e2: Expr<_, _> = app(app(app(g,
-                            App(bx(Builtin(Optional)), a0.clone())),
-                            Lam("x", a0.clone(), bx(OptionalLit(Some(a0.clone()), vec![Var(V("x", 0))])))), OptionalLit(Some(a0), vec![]));
+                        App(bx(Builtin(Optional)), a0.clone())),
+                            Lam("x", a0.clone(),
+                                bx(OptionalLit(Some(a0.clone()), vec![Var(V("x", 0))])))),
+                            OptionalLit(Some(a0), vec![]));
                     normalize(&e2)
                 }
                 (f2, a2) => app(f2, a2),
diff --git a/dhall/src/grammar_util.rs b/dhall/src/grammar_util.rs
index c185632..ce73444 100644
--- a/dhall/src/grammar_util.rs
+++ b/dhall/src/grammar_util.rs
@@ -3,5 +3,5 @@ use crate::core::{Expr, X};
 pub type ParsedExpr<'i> = Expr<'i, X, X>; // FIXME Parse paths and replace the second X with Path
 pub type BoxExpr<'i> = Box<ParsedExpr<'i>>;
 pub type ExprOpFn<'i> = fn(BoxExpr<'i>, BoxExpr<'i>) -> ParsedExpr<'i>;
-pub type ExprListFn<'i> = fn(Option<BoxExpr<'i>>, Vec<ParsedExpr<'i>>) -> ParsedExpr<'i>;
-
+pub type ExprListFn<'i> =
+    fn(Option<BoxExpr<'i>>, Vec<ParsedExpr<'i>>) -> ParsedExpr<'i>;
diff --git a/dhall/src/lexer.rs b/dhall/src/lexer.rs
index b5cbe6b..5fc0f05 100644
--- a/dhall/src/lexer.rs
+++ b/dhall/src/lexer.rs
@@ -1,8 +1,8 @@
 use nom::*;
 
-use crate::core::Const;
 use crate::core::Builtin;
 use crate::core::Builtin::*;
+use crate::core::Const;
 
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub enum Keyword {
@@ -74,11 +74,13 @@ fn is_identifier_rest_char(c: char) -> bool {
 
 macro_rules! digits {
     ($i:expr, $t:tt, $radix:expr) => {{
-        let r: nom::IResult<&str, $t> =
-            map_res!($i, take_while1_s!(call!(|c: char| c.is_digit($radix))),
-                     |s| $t::from_str_radix(s, $radix));
+        let r: nom::IResult<&str, $t> = map_res!(
+            $i,
+            take_while1_s!(call!(|c: char| c.is_digit($radix))),
+            |s| $t::from_str_radix(s, $radix)
+        );
         r
-    }}
+    }};
 }
 
 named!(natural<&str, usize>, digits!(usize, 10));
@@ -105,29 +107,32 @@ macro_rules! ident_tag {
                 if s == $tag {
                     nom::IResult::Done(i, s)
                 } else {
-                    nom::IResult::Error(error_position!(nom::ErrorKind::Tag, $i))
+                    nom::IResult::Error(error_position!(
+                        nom::ErrorKind::Tag,
+                        $i
+                    ))
                 }
             }
             r => r,
         }
-    }
+    };
 }
 
 fn string_escape_single(c: char) -> Option<&'static str> {
     match c {
-        'n'  => Some("\n"),
-        'r'  => Some("\r"),
-        't'  => Some("\t"),
-        '"'  => Some("\""),
+        'n' => Some("\n"),
+        'r' => Some("\r"),
+        't' => Some("\t"),
+        '"' => Some("\""),
         '\'' => Some("'"),
         '\\' => Some("\\"),
-        '0'  => Some("\0"),
-        'a'  => Some("\x07"),
-        'b'  => Some("\x08"),
-        'f'  => Some("\x0c"),
-        'v'  => Some("\x0b"),
-        '&'  => Some(""),
-        _    => None,
+        '0' => Some("\0"),
+        'a' => Some("\x07"),
+        'b' => Some("\x08"),
+        'f' => Some("\x0c"),
+        'v' => Some("\x0b"),
+        '&' => Some(""),
+        _ => None,
     }
 }
 
@@ -138,41 +143,53 @@ named!(string_escape_numeric<&str, char>, map_opt!(alt!(
 ), ::std::char::from_u32));
 
 fn string_lit_inner(input: &str) -> nom::IResult<&str, String> {
-    use nom::IResult::*;;
     use nom::ErrorKind;
+    use nom::IResult::*; ;
     let mut s = String::new();
     let mut cs = input.char_indices().peekable();
-    while let Some((i, c)) = cs.next()  {
+    while let Some((i, c)) = cs.next() {
         match c {
             '"' => return nom::IResult::Done(&input[i..], s),
             '\\' => match cs.next() {
                 Some((_, s)) if s.is_whitespace() => {
-                    while cs.peek().map(|&(_, s)| s.is_whitespace()) == Some(true) {
+                    while cs.peek().map(|&(_, s)| s.is_whitespace())
+                        == Some(true)
+                    {
                         let _ = cs.next();
                     }
                     if cs.next().map(|p| p.1) != Some('\\') {
-                        return Error(error_position!(ErrorKind::Custom(4 /* FIXME */), input));
+                        return Error(error_position!(
+                            ErrorKind::Custom(4 /* FIXME */),
+                            input
+                        ));
                     }
                 }
                 Some((j, ec)) => {
                     if let Some(esc) = string_escape_single(ec) {
                         s.push_str(esc);
-                        // FIXME Named ASCII escapes and control character escapes
+                    // FIXME Named ASCII escapes and control character escapes
                     } else {
                         match string_escape_numeric(&input[j..]) {
                             Done(rest, esc) => {
                                 let &(k, _) = cs.peek().unwrap();
                                 // digits are always single byte ASCII characters
                                 let consumed = input[k..].len() - rest.len();
-                                for _ in 0..consumed { let _ = cs.next(); }
+                                for _ in 0..consumed {
+                                    let _ = cs.next();
+                                }
                                 s.push(esc);
                             }
                             Incomplete(s) => return Incomplete(s),
                             Error(e) => return Error(e),
                         }
                     }
-                },
-                _ => return Error(error_position!(ErrorKind::Custom(5 /* FIXME */), input)),
+                }
+                _ => {
+                    return Error(error_position!(
+                        ErrorKind::Custom(5 /* FIXME */),
+                        input
+                    ));
+                }
             },
             _ => s.push(c),
         }
@@ -303,7 +320,8 @@ impl<'input> Lexer<'input> {
             "{-" => find_end(input, "-}"),
             "--" => find_end(input, "\n"), // Also skips past \r\n (CRLF)
             _ => None,
-        }.unwrap_or(0);
+        }
+        .unwrap_or(0);
         // println!("skipped {} bytes of comment", skip);
         self.offset += skip;
         skip != 0
@@ -337,9 +355,7 @@ impl<'input> Iterator for Lexer<'input> {
                 self.offset = self.input.len();
                 Some(Err(LexicalError::Error(offset, e)))
             }
-            Incomplete(needed) => {
-                Some(Err(LexicalError::Incomplete(needed)))
-            }
+            Incomplete(needed) => Some(Err(LexicalError::Incomplete(needed))),
         }
     }
 }
@@ -348,23 +364,31 @@ impl<'input> Iterator for Lexer<'input> {
 fn test_lex() {
     use self::Tok::*;
     let s = "λ(b : Bool) → b == False";
-    let expected = [Lambda,
-                    ParenL,
-                    Identifier("b"),
-                    Ascription,
-                    Builtin(crate::core::Builtin::Bool),
-                    ParenR,
-                    Arrow,
-                    Identifier("b"),
-                    CompareEQ,
-                    Bool(false)];
+    let expected = [
+        Lambda,
+        ParenL,
+        Identifier("b"),
+        Ascription,
+        Builtin(crate::core::Builtin::Bool),
+        ParenR,
+        Arrow,
+        Identifier("b"),
+        CompareEQ,
+        Bool(false),
+    ];
     let lexer = Lexer::new(s);
     let tokens = lexer.map(|r| r.unwrap().1).collect::<Vec<_>>();
     assert_eq!(&tokens, &expected);
 
     assert_eq!(string_lit(r#""a\&b""#).to_result(), Ok("ab".to_owned()));
-    assert_eq!(string_lit(r#""a\     \b""#).to_result(), Ok("ab".to_owned()));
+    assert_eq!(
+        string_lit(r#""a\     \b""#).to_result(),
+        Ok("ab".to_owned())
+    );
     assert!(string_lit(r#""a\     b""#).is_err());
     assert_eq!(string_lit(r#""a\nb""#).to_result(), Ok("a\nb".to_owned()));
-    assert_eq!(string_lit(r#""\o141\x62\99""#).to_result(), Ok("abc".to_owned()));
+    assert_eq!(
+        string_lit(r#""\o141\x62\99""#).to_result(),
+        Ok("abc".to_owned())
+    );
 }
diff --git a/dhall/src/main.rs b/dhall/src/main.rs
index 58826bb..78a2905 100644
--- a/dhall/src/main.rs
+++ b/dhall/src/main.rs
@@ -1,5 +1,5 @@
-use std::io::{self, Read};
 use std::error::Error;
+use std::io::{self, Read};
 use term_painter::ToStyle;
 
 use dhall::*;
@@ -42,9 +42,13 @@ fn print_error(message: &str, source: &str, start: usize, end: usize) {
     BOLD.with(|| {
         print!("{:w$} |", "", w = line_number_width);
         ERROR_STYLE.with(|| {
-            println!(" {:so$}{:^>ew$}", "", "",
-                     so = source[line_start..start].chars().count(),
-                     ew = ::std::cmp::max(1, source[start..end].chars().count()));
+            println!(
+                " {:so$}{:^>ew$}",
+                "",
+                "",
+                so = source[line_start..start].chars().count(),
+                ew = ::std::cmp::max(1, source[start..end].chars().count())
+            );
         });
     });
 }
@@ -54,12 +58,27 @@ fn main() {
     io::stdin().read_to_string(&mut buffer).unwrap();
     let expr = match parser::parse_expr_lalrpop(&buffer) {
         Ok(e) => e,
-        Err(lalrpop_util::ParseError::User { error: lexer::LexicalError::Error(pos, e) }) => {
-            print_error(&format!("Unexpected token {:?}", e), &buffer, pos, pos);
+        Err(lalrpop_util::ParseError::User {
+            error: lexer::LexicalError::Error(pos, e),
+        }) => {
+            print_error(
+                &format!("Unexpected token {:?}", e),
+                &buffer,
+                pos,
+                pos,
+            );
             return;
         }
-        Err(lalrpop_util::ParseError::UnrecognizedToken { token: Some((start, t, end)), expected: e }) => {
-            print_error(&format!("Unrecognized token {:?}", t), &buffer, start, end);
+        Err(lalrpop_util::ParseError::UnrecognizedToken {
+            token: Some((start, t, end)),
+            expected: e,
+        }) => {
+            print_error(
+                &format!("Unrecognized token {:?}", t),
+                &buffer,
+                start,
+                end,
+            );
             if !e.is_empty() {
                 println!("Expected {:?}", e);
             }
diff --git a/dhall/src/parser.rs b/dhall/src/parser.rs
index 303e2ad..6b20c01 100644
--- a/dhall/src/parser.rs
+++ b/dhall/src/parser.rs
@@ -7,7 +7,7 @@ use pest::Parser;
 use dhall_parser::{DhallParser, Rule};
 
 use crate::core;
-use crate::core::{bx, Builtin, Const, Expr, BinOp, V};
+use crate::core::{bx, BinOp, Builtin, Const, Expr, V};
 use crate::grammar;
 use crate::grammar_util::{BoxExpr, ParsedExpr};
 use crate::lexer::{Lexer, LexicalError, Tok};
@@ -762,8 +762,8 @@ pub fn parse_expr_pest(s: &str) -> ParseResult<BoxExpr> {
 
 #[test]
 fn test_parse() {
-    use crate::core::Expr::*;
     use crate::core::BinOp::*;
+    use crate::core::Expr::*;
     // let expr = r#"{ x = "foo", y = 4 }.x"#;
     // let expr = r#"(1 + 2) * 3"#;
     let expr = r#"if True then 1 + 3 * 5 else 2"#;
@@ -790,9 +790,11 @@ fn test_parse() {
     assert!(parse_expr_lalrpop("(22)").is_ok());
     assert_eq!(
         parse_expr_lalrpop("3 + 5 * 10").ok(),
-        Some(Box::new(BinOp(NaturalPlus,
+        Some(Box::new(BinOp(
+            NaturalPlus,
             Box::new(NaturalLit(3)),
-            Box::new(BinOp(NaturalTimes,
+            Box::new(BinOp(
+                NaturalTimes,
                 Box::new(NaturalLit(5)),
                 Box::new(NaturalLit(10))
             ))
@@ -801,9 +803,11 @@ fn test_parse() {
     // The original parser is apparently right-associative
     assert_eq!(
         parse_expr_lalrpop("2 * 3 * 4").ok(),
-        Some(Box::new(BinOp(NaturalTimes,
+        Some(Box::new(BinOp(
+            NaturalTimes,
             Box::new(NaturalLit(2)),
-            Box::new(BinOp(NaturalTimes,
+            Box::new(BinOp(
+                NaturalTimes,
                 Box::new(NaturalLit(3)),
                 Box::new(NaturalLit(4))
             ))
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 90e5f55..976293d 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -5,15 +5,17 @@ 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::Builtin::*;
 use crate::core::Const::*;
 use crate::core::Expr::*;
+use crate::core::{app, pi};
+use crate::core::{bx, normalize, shift, subst, Expr, V, X};
 
 use self::TypeMessage::*;
 
-fn axiom<'i, S: Clone>(c: core::Const) -> Result<core::Const, TypeError<'i, S>> {
+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)),
@@ -24,8 +26,7 @@ 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),
+        (Type, Type) | (Kind, Type) => Ok(Type),
     }
 }
 
@@ -33,7 +34,11 @@ 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, 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 };
@@ -43,16 +48,21 @@ fn match_vars(vl: &V, vr: &V, ctx: &[(&str, &str)]) -> bool {
 }
 
 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
+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
+    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,
+            (&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
@@ -68,8 +78,13 @@ fn prop_equal<S, T>(eL0: &Expr<S, X>, eR0: &Expr<T, X>) -> bool
                     false
                 }
             }
-            (&App(ref fL, ref aL), &App(ref fR, ref aR)) =>
-                if go(ctx, fL, fR) { go(ctx, aL, aR) } else { false },
+            (&App(ref fL, ref aL), &App(ref fR, ref aR)) => {
+                if go(ctx, fL, fR) {
+                    go(ctx, aL, aR)
+                } else {
+                    false
+                }
+            }
             (&Builtin(a), &Builtin(b)) => a == b,
             (&Record(ref ktsL0), &Record(ref ktsR0)) => {
                 if ktsL0.len() != ktsR0.len() {
@@ -97,28 +112,30 @@ fn prop_equal<S, T>(eL0: &Expr<S, X>, eR0: &Expr<T, X>) -> bool
                 }
                 true
                 */
-                !ktsL0.iter().zip(ktsR0.iter()).any(|((kL, tL), (kR, tR))| {
-                    kL != kR || !go(ctx, tL, tR)
-                })
+                !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)
-                })
+                /*
+                    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,
         }
@@ -127,15 +144,17 @@ fn prop_equal<S, T>(eL0: &Expr<S, X>, eR0: &Expr<T, X>) -> bool
     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::Builtin,
-                       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>,
+fn op2_type<'i, S, EF>(
+    ctx: &Context<'i, Expr<'i, S, X>>,
+    e: &Expr<'i, S, X>,
+    t: core::Builtin,
+    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 {
@@ -158,10 +177,12 @@ fn op2_type<'i, S, EF>(ctx: &Context<'i, Expr<'i, S, X>>,
 /// `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
+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,
 {
     use crate::BinOp::*;
     match *e {
@@ -173,7 +194,9 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
                 .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 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)?;
@@ -184,18 +207,32 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
             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()))),
+                _ => {
+                    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 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))),
+                _ => {
+                    return Err(TypeError::new(&ctx2, e, InvalidOutputType(tB)));
+                }
             };
 
             match rule(kA, kB) {
-                Err(()) => Err(TypeError::new(ctx, e, NoDependentTypes((**tA).clone(), tB))),
+                Err(()) => Err(TypeError::new(
+                    ctx,
+                    e,
+                    NoDependentTypes((**tA).clone(), tB),
+                )),
                 Ok(k) => Ok(Const(k)),
             }
         }
@@ -203,39 +240,49 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
             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))),
+                _ => {
+                    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 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_A = normalize(&tA);
                 let nf_A2 = normalize(&tA2);
-                Err(TypeError::new(ctx, e, TypeMismatch((**f).clone(), nf_A, (**a).clone(), nf_A2)))
+                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 tR = type_with(ctx, r)?;
             let ttR = normalize::<S, S, X>(&type_with(ctx, &tR)?);
-            let kR  = match ttR {
+            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))),
+                _ => return Err(TypeError::new(ctx, e, InvalidInputType(tR))),
             };
 
             let ctx2 = ctx.insert(f, tR.clone());
-            let tB  = type_with(&ctx2, b)?;
+            let tB = type_with(&ctx2, b)?;
             let ttB = normalize::<S, S, X>(&type_with(ctx, &tB)?);
-            let kB  = match ttB {
+            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))),
+                _ => return Err(TypeError::new(ctx, e, InvalidOutputType(tB))),
             };
 
             if let Err(()) = rule(kR, kB) {
@@ -243,10 +290,14 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
             }
 
             if let Some(ref t) = *mt {
-                let nf_t  = normalize(t);
+                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)));
+                    return Err(TypeError::new(
+                        ctx,
+                        e,
+                        AnnotMismatch((**r).clone(), nf_t, nf_tR),
+                    ));
                 }
             }
 
@@ -260,9 +311,13 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
             if prop_equal(t, &t2) {
                 Ok((**t).clone())
             } else {
-                let nf_t  = normalize(t);
+                let nf_t = normalize(t);
                 let nf_t2 = normalize(&t2);
-                Err(TypeError::new(ctx, e, AnnotMismatch((**x).clone(), nf_t, nf_t2)))
+                Err(TypeError::new(
+                    ctx,
+                    e,
+                    AnnotMismatch((**x).clone(), nf_t, nf_t2),
+                ))
             }
         }
         BoolLit(_) => Ok(Builtin(Bool)),
@@ -274,48 +329,91 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
             let tx = normalize(&type_with(ctx, x)?);
             match tx {
                 Builtin(Bool) => {}
-                _ => return Err(TypeError::new(ctx, e, InvalidPredicate((**x).clone(), tx))),
+                _ => {
+                    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))),
+                _ => {
+                    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))),
+                _ => {
+                    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)));
+                return Err(TypeError::new(
+                    ctx,
+                    e,
+                    IfBranchMismatch((**y).clone(), (**z).clone(), ty, tz),
+                ));
             }
             Ok(ty)
         }
         NaturalLit(_) => Ok(Builtin(Natural)),
-        Builtin(NaturalFold) =>
-            Ok(pi("_", Natural,
-                pi("natural", Const(Type),
-                    pi("succ", pi("_", "natural", "natural"),
-                        pi("zero", "natural", "natural"))))),
-        Builtin(NaturalBuild) =>
-            Ok(pi("_",
-                pi("natural", Const(Type),
-                    pi("succ", pi("_", "natural", "natural"),
-                        pi("zero", "natural", "natural"))),
-                Natural)),
-        Builtin(NaturalIsZero) |
-        Builtin(NaturalEven) |
-        Builtin(NaturalOdd) => Ok(pi("_", Natural, Bool)),
-        BinOp(NaturalPlus, ref l, ref r) => op2_type(ctx, e, Natural, CantAdd, l, r),
-        BinOp(NaturalTimes, ref l, ref r) => op2_type(ctx, e, Natural, CantMultiply, l, r),
+        Builtin(NaturalFold) => Ok(pi(
+            "_",
+            Natural,
+            pi(
+                "natural",
+                Const(Type),
+                pi(
+                    "succ",
+                    pi("_", "natural", "natural"),
+                    pi("zero", "natural", "natural"),
+                ),
+            ),
+        )),
+        Builtin(NaturalBuild) => Ok(pi(
+            "_",
+            pi(
+                "natural",
+                Const(Type),
+                pi(
+                    "succ",
+                    pi("_", "natural", "natural"),
+                    pi("zero", "natural", "natural"),
+                ),
+            ),
+            Natural,
+        )),
+        Builtin(NaturalIsZero) | Builtin(NaturalEven) | Builtin(NaturalOdd) => {
+            Ok(pi("_", Natural, Bool))
+        }
+        BinOp(NaturalPlus, ref l, ref r) => {
+            op2_type(ctx, e, Natural, CantAdd, l, r)
+        }
+        BinOp(NaturalTimes, ref l, ref r) => {
+            op2_type(ctx, e, Natural, CantMultiply, l, r)
+        }
         IntegerLit(_) => Ok(Builtin(Integer)),
         DoubleLit(_) => Ok(Builtin(Double)),
         TextLit(_) => Ok(Builtin(Text)),
-        BinOp(TextAppend, ref l, ref r) => op2_type(ctx, e, Text, CantTextAppend, l, r),
+        BinOp(TextAppend, ref l, ref r) => {
+            op2_type(ctx, e, Text, CantTextAppend, l, r)
+        }
         ListLit(ref t, ref xs) => {
             let mut iter = xs.iter().enumerate();
             let t: Box<Expr<_, _>> = match t {
@@ -323,7 +421,7 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
                 None => {
                     let (_, first_x) = iter.next().unwrap();
                     bx(type_with(ctx, first_x)?)
-                },
+                }
             };
 
             let s = normalize::<_, S, _>(&type_with(ctx, &t)?);
@@ -334,39 +432,74 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
             for (i, x) in iter {
                 let t2 = type_with(ctx, x)?;
                 if !prop_equal(&t, &t2) {
-                    let nf_t  = normalize(&t);
+                    let nf_t = normalize(&t);
                     let nf_t2 = normalize(&t2);
-                    return Err(TypeError::new(ctx, e, InvalidListElement(i, nf_t, x.clone(), nf_t2)) )
+                    return Err(TypeError::new(
+                        ctx,
+                        e,
+                        InvalidListElement(i, nf_t, x.clone(), nf_t2),
+                    ));
                 }
             }
             Ok(App(bx(Builtin(List)), t))
         }
-        Builtin(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")))),
-        Builtin(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")))))),
-        Builtin(ListLength) =>
-            Ok(pi("a", Const(Type), pi("_", app(List, "a"), Natural))),
-        Builtin(ListHead) |
-        Builtin(ListLast) =>
-            Ok(pi("a", Const(Type), pi("_", app(List, "a"), app(Optional, "a")))),
+        Builtin(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"),
+            ),
+        )),
+        Builtin(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"),
+                    ),
+                ),
+            ),
+        )),
+        Builtin(ListLength) => {
+            Ok(pi("a", Const(Type), pi("_", app(List, "a"), Natural)))
+        }
+        Builtin(ListHead) | Builtin(ListLast) => Ok(pi(
+            "a",
+            Const(Type),
+            pi("_", app(List, "a"), app(Optional, "a")),
+        )),
         Builtin(ListIndexed) => {
             let mut m = BTreeMap::new();
             m.insert("index", Builtin(Natural));
             m.insert("value", Expr::from("a"));
-            Ok(pi("a", Const(Type), pi("_", app(List, "a"), app(List, Record(m)))))
+            Ok(pi(
+                "a",
+                Const(Type),
+                pi("_", app(List, "a"), app(List, Record(m))),
+            ))
         }
-        Builtin(ListReverse) =>
-            Ok(pi("a", Const(Type), pi("_", app(List, "a"), app(List, "a")))),
+        Builtin(ListReverse) => Ok(pi(
+            "a",
+            Const(Type),
+            pi("_", app(List, "a"), app(List, "a")),
+        )),
         OptionalLit(ref t, ref xs) => {
             let mut iter = xs.iter();
             let t: Box<Expr<_, _>> = match t {
@@ -374,13 +507,15 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
                 None => {
                     let first_x = iter.next().unwrap();
                     bx(type_with(ctx, first_x)?)
-                },
+                }
             };
 
             let s = normalize::<_, S, _>(&type_with(ctx, &t)?);
             match s {
                 Const(Type) => {}
-                _ => return Err(TypeError::new(ctx, e, InvalidOptionalType(*t))),
+                _ => {
+                    return Err(TypeError::new(ctx, e, InvalidOptionalType(*t)));
+                }
             }
             let n = xs.len();
             if 2 <= n {
@@ -389,140 +524,180 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
             for x in iter {
                 let t2 = type_with(ctx, x)?;
                 if !prop_equal(&t, &t2) {
-                    let nf_t  = normalize(&t);
+                    let nf_t = normalize(&t);
                     let nf_t2 = normalize(&t2);
-                    return Err(TypeError::new(ctx, e, InvalidOptionalElement(nf_t, x.clone(), nf_t2)));
+                    return Err(TypeError::new(
+                        ctx,
+                        e,
+                        InvalidOptionalElement(nf_t, x.clone(), nf_t2),
+                    ));
                 }
             }
             Ok(App(bx(Builtin(Optional)), t))
         }
-        Builtin(OptionalFold) =>
-            Ok(pi("a", Const(Type),
-                pi("_", app(Optional, "a"),
-                    pi("optional", Const(Type),
-                        pi("just", pi("_", "a", "optional"),
-                            pi("nothing", "optional", "optional")))))),
-        Builtin(List) | Builtin(Optional) =>
-            Ok(pi("_", Const(Type), Const(Type))),
-        Builtin(Bool) | Builtin(Natural) | Builtin(Integer) | Builtin(Double) | Builtin(Text) =>
-            Ok(Const(Type)),
+        Builtin(OptionalFold) => Ok(pi(
+            "a",
+            Const(Type),
+            pi(
+                "_",
+                app(Optional, "a"),
+                pi(
+                    "optional",
+                    Const(Type),
+                    pi(
+                        "just",
+                        pi("_", "a", "optional"),
+                        pi("nothing", "optional", "optional"),
+                    ),
+                ),
+            ),
+        )),
+        Builtin(List) | Builtin(Optional) => {
+            Ok(pi("_", Const(Type), Const(Type)))
+        }
+        Builtin(Bool) | Builtin(Natural) | Builtin(Integer)
+        | Builtin(Double) | Builtin(Text) => Ok(Const(Type)),
         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()))),
+                    _ => {
+                        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<_, _>>()?;
+            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
-    */
+        /*
+        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()))),
+                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
-*/
+        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),
     }
@@ -531,7 +706,9 @@ type_with ctx   (Note s e'       ) = case type_with ctx e' of
 /// `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>> {
+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())
 }
@@ -543,7 +720,12 @@ pub enum TypeMessage<'i, S> {
     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>),
+    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>),
@@ -552,7 +734,12 @@ pub enum TypeMessage<'i, S> {
     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>),
+    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>),
@@ -590,10 +777,11 @@ pub struct TypeError<'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 {
+    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(),
@@ -618,7 +806,9 @@ impl<'i, S: fmt::Debug> ::std::error::Error for TypeMessage<'i, S> {
 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")),
+            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
diff --git a/dhall/tests/macros.rs b/dhall/tests/macros.rs
index 131683b..66b9dbf 100644
--- a/dhall/tests/macros.rs
+++ b/dhall/tests/macros.rs
@@ -1,27 +1,34 @@
 #[macro_export]
 macro_rules! include_test_str {
-    ($x:expr) => { include_str!(concat!("../../dhall-lang/tests/", $x, ".dhall")) };
+    ($x:expr) => {
+        include_str!(concat!("../../dhall-lang/tests/", $x, ".dhall"))
+    };
 }
 
 #[macro_export]
 macro_rules! include_test_strs_ab {
-    ($x:expr) => { (include_test_str!(concat!($x, "A")), include_test_str!(concat!($x, "B"))) };
+    ($x:expr) => {
+        (
+            include_test_str!(concat!($x, "A")),
+            include_test_str!(concat!($x, "B")),
+        )
+    };
 }
 
 #[macro_export]
 macro_rules! parse_str {
-    ($str:expr) => {
-        {
-            let pest_expr = parser::parse_expr_pest(&$str).map_err(|e| println!("{}", e)).unwrap();
-            // // Check with old parser
-            // match parser::parse_expr_lalrpop(&$str) {
-            //     Ok(larlpop_expr) => assert_eq!(pest_expr, larlpop_expr),
-            //     Err(_) => {},
-            // };
-            // panic!("{:?}", pest_expr);
-            pest_expr
-        }
-    };
+    ($str:expr) => {{
+        let pest_expr = parser::parse_expr_pest(&$str)
+            .map_err(|e| println!("{}", e))
+            .unwrap();
+        // // Check with old parser
+        // match parser::parse_expr_lalrpop(&$str) {
+        //     Ok(larlpop_expr) => assert_eq!(pest_expr, larlpop_expr),
+        //     Err(_) => {},
+        // };
+        // panic!("{:?}", pest_expr);
+        pest_expr
+    }};
 }
 
 #[macro_export]
@@ -60,7 +67,10 @@ macro_rules! run_spec_test {
         let (expr_str, expected_str) = include_test_strs_ab!($path);
         let expr = parse_str!(expr_str);
         let expected = parse_str!(expected_str);
-        assert_eq_!(normalize::<_, X, _>(&expr), normalize::<_, X, _>(&expected));
+        assert_eq_!(
+            normalize::<_, X, _>(&expr),
+            normalize::<_, X, _>(&expected)
+        );
     };
     (parser, $path:expr) => {
         let expr_str = include_test_str!(concat!($path, "A"));
@@ -79,13 +89,18 @@ macro_rules! make_spec_test {
         #[allow(non_snake_case)]
         #[allow(unused_variables)]
         #[allow(unused_imports)]
-        fn $name(){
-            use std::thread;
+        fn $name() {
             use dhall::*;
+            use std::thread;
 
-            thread::Builder::new().stack_size(16 * 1024 * 1024).spawn(move || {
-                run_spec_test!($type, $path);
-            }).unwrap().join().unwrap();
+            thread::Builder::new()
+                .stack_size(16 * 1024 * 1024)
+                .spawn(move || {
+                    run_spec_test!($type, $path);
+                })
+                .unwrap()
+                .join()
+                .unwrap();
         }
     };
 }
diff --git a/dhall_parser/build.rs b/dhall_parser/build.rs
index 743aa2d..a206517 100644
--- a/dhall_parser/build.rs
+++ b/dhall_parser/build.rs
@@ -1,8 +1,8 @@
-use std::fs::File;
-use std::io::{Read,Write,BufReader,BufRead};
 use std::collections::HashMap;
+use std::fs::File;
+use std::io::{BufRead, BufReader, Read, Write};
 
-use abnf_to_pest::{PestRuleSettings, abnf_to_pest};
+use abnf_to_pest::{abnf_to_pest, PestRuleSettings};
 
 fn main() -> std::io::Result<()> {
     // TODO: upstream changes to grammar
@@ -22,26 +22,47 @@ fn main() -> std::io::Result<()> {
     for line in BufReader::new(File::open(visibility_path)?).lines() {
         let line = line?;
         if line.len() >= 2 && &line[0..2] == "# " {
-            rule_settings.insert(line[2..].into(), PestRuleSettings { visible: false, ..Default::default() });
+            rule_settings.insert(
+                line[2..].into(),
+                PestRuleSettings {
+                    visible: false,
+                    ..Default::default()
+                },
+            );
         } else {
-            rule_settings.insert(line, PestRuleSettings { visible: true, ..Default::default() });
+            rule_settings.insert(
+                line,
+                PestRuleSettings {
+                    visible: true,
+                    ..Default::default()
+                },
+            );
         }
     }
-    rule_settings.insert("simple_label".to_owned(), PestRuleSettings {
-        visible: true,
-        replace: Some("
+    rule_settings.insert(
+        "simple_label".to_owned(),
+        PestRuleSettings {
+            visible: true,
+            replace: Some(
+                "
               keyword_raw ~ simple_label_next_char+
             | !keyword_raw ~ simple_label_first_char ~ simple_label_next_char*
-        ".to_owned()),
-    });
+        "
+                .to_owned(),
+            ),
+        },
+    );
 
     let mut file = File::create(pest_path)?;
     writeln!(&mut file, "// AUTO-GENERATED FILE. See build.rs.")?;
     writeln!(&mut file, "{}", abnf_to_pest(&data, &rule_settings)?)?;
-    writeln!(&mut file, "keyword_raw = _{{
+    writeln!(
+        &mut file,
+        "keyword_raw = _{{
         let_raw | in_raw | if_raw | then_raw
             | else_raw | Infinity_raw | NaN_raw
-    }}")?;
+    }}"
+    )?;
     writeln!(
         &mut file,
         "final_expression = {{ SOI ~ complete_expression ~ EOI }}"