Slowly propagate the new type parameter throughout the codebase

4 files changed, 103 insertions, 80 deletions

diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
index 4e183b4..6372768 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -43,7 +43,7 @@ impl fmt::Display for DhallError {
 pub fn load_dhall_file<'i, 'a: 'i>(
     f: &Path,
     source_pool: &'a mut Vec<String>,
-    resolve_imports: bool,
+    _resolve_imports: bool,
 ) -> Result<Expr<'i, X, X>, DhallError> {
     source_pool.push(String::new());
     let mut buffer = source_pool.last_mut().unwrap();
diff --git a/dhall/src/main.rs b/dhall/src/main.rs
index 493f9be..dbe80a3 100644
--- a/dhall/src/main.rs
+++ b/dhall/src/main.rs
@@ -89,5 +89,5 @@ fn main() {
 
     println!("{}", type_expr);
     println!("");
-    println!("{}", normalize::<_, X, _>(&expr));
+    println!("{}", normalize::<_, _, X, _>(&expr));
 }
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 246a3c0..d3766d5 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -12,7 +12,9 @@ use std::fmt;
 /// However, `normalize` will not fail if the expression is ill-typed and will
 /// leave ill-typed sub-expressions unevaluated.
 ///
-pub fn normalize<'i, S, T, A>(e: &Expr<'i, S, A>) -> Expr<'i, T, A>
+pub fn normalize<Label: StringLike, S, T, A>(
+    e: &Expr_<Label, S, A>,
+) -> Expr_<Label, T, A>
 where
     S: Clone + fmt::Debug,
     T: Clone + fmt::Debug,
@@ -24,9 +26,9 @@ where
     match e {
         // Matches that don't normalize everything right away
         Let(f, _, r, b) => {
-            let r2 = shift::<_, S, _>(1, V(f, 0), r);
-            let b2 = subst(V(f, 0), &r2, b);
-            let b3 = shift::<_, T, _>(-1, V(f, 0), &b2);
+            let r2 = shift::<Label, _, S, _>(1, V(f.clone(), 0), r);
+            let b2 = subst::<Label, _, S, _>(V(f.clone(), 0), &r2, b);
+            let b3 = shift::<Label, _, T, _>(-1, V(f.clone(), 0), &b2);
             normalize(&b3)
         }
         BoolIf(b, t, f) => match normalize(b) {
@@ -36,16 +38,16 @@ where
         },
         Annot(x, _) => normalize(x),
         Note(_, e) => normalize(e),
-        App(f, a) => match normalize::<S, T, A>(f) {
+        App(f, a) => match normalize::<Label, S, T, A>(f) {
             Lam(x, _A, b) => {
                 // Beta reduce
                 let vx0 = V(x, 0);
-                let a2 = shift::<S, S, A>(1, vx0, a);
-                let b2 = subst::<S, T, A>(vx0, &a2, &b);
-                let b3 = shift::<S, T, A>(-1, vx0, &b2);
+                let a2 = shift::<Label, S, S, A>(1, vx0, a);
+                let b2 = subst::<Label, S, T, A>(vx0, &a2, &b);
+                let b3 = shift::<Label, S, T, A>(-1, vx0, &b2);
                 normalize(&b3)
             }
-            f2 => match (f2, normalize::<S, T, A>(a)) {
+            f2 => match (f2, normalize::<Label, S, T, A>(a)) {
                 // fold/build fusion for `List`
                 (App(box Builtin(ListBuild), _), App(box App(box Builtin(ListFold), _), box e2)) |
                 (App(box Builtin(ListFold), _), App(box App(box Builtin(ListBuild), _), box e2)) |
@@ -87,13 +89,14 @@ where
                 (Builtin(NaturalOdd), NaturalLit(n)) => BoolLit(n % 2 != 0),
                 (Builtin(NaturalToInteger), NaturalLit(n)) => IntegerLit(n as isize),
                 (Builtin(NaturalShow), NaturalLit(n)) => TextLit(n.to_string()),
-                (App(box Builtin(ListBuild), a0), k) => {
-                    let k = bx(k);
-                    let a1 = bx(shift(1, V("a", 0), &a0));
-                    normalize(&dhall!(k (List a0) (λ(a : a0) -> λ(as : List a1) -> [ a ] # as) ([] : List a0)))
-                }
+                // TODO: restore when handling variables generically fixed
+                // (App(box Builtin(ListBuild), a0), k) => {
+                //     let k = bx(k);
+                //     let a1 = bx(shift(1, V("a", 0), &a0));
+                //     normalize(&dhall!(k (List a0) (λ(a : a0) -> λ(as : List a1) -> [ a ] # as) ([] : List a0)))
+                // }
                 (App(box App(box App(box App(box Builtin(ListFold), _), box ListLit(_, xs)), _), cons), nil) => {
-                    let e2: Expr<_, _> = xs.into_iter().rev().fold(nil, |y, ys| {
+                    let e2: Expr_<_, _, _> = xs.into_iter().rev().fold(nil, |y, ys| {
                         let y = bx(y);
                         let ys = bx(ys);
                         dhall!(cons y ys)
@@ -130,23 +133,29 @@ where
                               ]
             */
                 (App(box App(box App(box App(box Builtin(OptionalFold), _), box OptionalLit(_, xs)), _), just), nothing) => {
-                    let e2: Expr<_, _> = xs.into_iter().fold(nothing, |y, _| {
+                    let e2: Expr_<_, _, _> = xs.into_iter().fold(nothing, |y, _| {
                         let y = bx(y);
                         dhall!(just y)
                     });
                     normalize(&e2)
                 }
-                (App(box Builtin(OptionalBuild), a0), g) => {
-                    let g = bx(g);
-                    normalize(&dhall!((g (Optional a0)) (λ(x: a0) -> [x] :  Optional a0) ([] :  Optional a0)))
-                }
+                // TODO: restore when handling variables generically fixed
+                // (App(box Builtin(OptionalBuild), a0), g) => {
+                //     let g = bx(g);
+                //     normalize(&dhall!((g (Optional a0)) (λ(x: a0) -> [x] :  Optional a0) ([] :  Optional a0)))
+                // }
                 (f2, a2) => app(f2, a2),
             },
         },
 
         // Normalize everything else before matching
         e => {
-            match e.map_shallow(normalize, |_| unreachable!(), |x| x.clone()) {
+            match e.map_shallow(
+                normalize,
+                |_| unreachable!(),
+                |x| x.clone(),
+                |x| x.clone(),
+            ) {
                 BinOp(BoolAnd, box BoolLit(x), box BoolLit(y)) => {
                     BoolLit(x && y)
                 }
@@ -180,7 +189,7 @@ where
                     ListLit(t, xs.chain(ys).collect())
                 }
                 Merge(_x, _y, _t) => unimplemented!(),
-                Field(box RecordLit(kvs), x) => match kvs.get(x) {
+                Field(box RecordLit(kvs), x) => match kvs.get(&x) {
                     Some(r) => r.clone(),
                     None => Field(bx(RecordLit(kvs)), x),
                 },
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 23ab7a6..c2a2ca3 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -10,7 +10,7 @@ use dhall_core::core::Builtin::*;
 use dhall_core::core::Const::*;
 use dhall_core::core::Expr_::*;
 use dhall_core::core::{app, pi};
-use dhall_core::core::{bx, shift, subst, Expr, V, X};
+use dhall_core::core::{bx, shift, subst, Expr, Expr_, V, X};
 
 use self::TypeMessage::*;
 
@@ -155,7 +155,7 @@ fn op2_type<'i, S, EF>(
 ) -> 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>,
+    EF: FnOnce(Expr<'i, S, X>, Expr<'i, S, X>) -> TypeMessage<&'i str, S>,
 {
     let tl = normalize(&type_with(ctx, l)?);
     match tl {
@@ -189,7 +189,7 @@ where
     use dhall_core::Expr_;
     match *e {
         Const(c) => axiom(c).map(Const), //.map(Cow::Owned),
-        Var(V(x, n)) => {
+        Var(V(ref x, n)) => {
             ctx.lookup(x, n)
                 .cloned()
                 //.map(Cow::Borrowed)
@@ -206,7 +206,7 @@ where
             Ok(p)
         }
         Pi(x, ref tA, ref tB) => {
-            let tA2 = normalize::<S, S, X>(&type_with(ctx, tA)?);
+            let tA2 = normalize::<_, S, S, X>(&type_with(ctx, tA)?);
             let kA = match tA2 {
                 Const(k) => k,
                 _ => {
@@ -253,9 +253,9 @@ where
             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::<&str, S, S, X>(1, vx0, a);
                 let tB2 = subst(vx0, &a2, &tB);
-                let tB3 = shift::<S, S, X>(-1, vx0, &tB2);
+                let tB3 = shift::<&str, S, S, X>(-1, vx0, &tB2);
                 Ok(tB3)
             } else {
                 let nf_A = normalize(&tA);
@@ -269,7 +269,7 @@ where
         }
         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 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
@@ -279,7 +279,7 @@ where
 
             let ctx2 = ctx.insert(f, tR.clone());
             let tB = type_with(&ctx2, b)?;
-            let ttB = normalize::<S, S, X>(&type_with(ctx, &tB)?);
+            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
@@ -426,7 +426,7 @@ where
                 }
             };
 
-            let s = normalize::<_, S, _>(&type_with(ctx, &t)?);
+            let s = normalize::<_, _, S, _>(&type_with(ctx, &t)?);
             match s {
                 Const(Type) => {}
                 _ => return Err(TypeError::new(ctx, e, InvalidListType(*t))),
@@ -512,7 +512,7 @@ where
                 }
             };
 
-            let s = normalize::<_, S, _>(&type_with(ctx, &t)?);
+            let s = normalize::<_, _, S, _>(&type_with(ctx, &t)?);
             match s {
                 Const(Type) => {}
                 _ => {
@@ -561,7 +561,7 @@ where
         | 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)?);
+                let s = normalize::<_, S, S, X>(&type_with(ctx, t)?);
                 match s {
                     Const(Type) => {}
                     _ => {
@@ -580,7 +580,7 @@ where
                 .iter()
                 .map(|(&k, v)| {
                     let t = type_with(ctx, v)?;
-                    let s = normalize::<S, S, X>(&type_with(ctx, &t)?);
+                    let s = normalize::<_, S, S, X>(&type_with(ctx, &t)?);
                     match s {
                         Const(Type) => {}
                         _ => {
@@ -717,57 +717,71 @@ pub fn type_of<'i, S: Clone + ::std::fmt::Debug + 'i>(
 
 /// The specific type error
 #[derive(Debug)]
-pub enum TypeMessage<'i, S> {
+pub enum TypeMessage<Label, S> {
     UnboundVariable,
-    InvalidInputType(Expr<'i, S, X>),
-    InvalidOutputType(Expr<'i, S, X>),
-    NotAFunction(Expr<'i, S, X>, Expr<'i, S, X>),
+    InvalidInputType(Expr_<Label, S, X>),
+    InvalidOutputType(Expr_<Label, S, X>),
+    NotAFunction(Expr_<Label, S, X>, Expr_<Label, S, X>),
     TypeMismatch(
-        Expr<'i, S, X>,
-        Expr<'i, S, X>,
-        Expr<'i, S, X>,
-        Expr<'i, S, X>,
+        Expr_<Label, S, X>,
+        Expr_<Label, S, X>,
+        Expr_<Label, S, X>,
+        Expr_<Label, S, X>,
     ),
-    AnnotMismatch(Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>),
+    AnnotMismatch(Expr_<Label, S, X>, Expr_<Label, S, X>, Expr_<Label, 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>),
+    InvalidListElement(
+        usize,
+        Expr_<Label, S, X>,
+        Expr_<Label, S, X>,
+        Expr_<Label, S, X>,
+    ),
+    InvalidListType(Expr_<Label, S, X>),
+    InvalidOptionalElement(
+        Expr_<Label, S, X>,
+        Expr_<Label, S, X>,
+        Expr_<Label, S, X>,
+    ),
     InvalidOptionalLiteral(usize),
-    InvalidOptionalType(Expr<'i, S, X>),
-    InvalidPredicate(Expr<'i, S, X>, Expr<'i, S, X>),
+    InvalidOptionalType(Expr_<Label, S, X>),
+    InvalidPredicate(Expr_<Label, S, X>, Expr_<Label, S, X>),
     IfBranchMismatch(
-        Expr<'i, S, X>,
-        Expr<'i, S, X>,
-        Expr<'i, S, X>,
-        Expr<'i, S, X>,
+        Expr_<Label, S, X>,
+        Expr_<Label, S, X>,
+        Expr_<Label, S, X>,
+        Expr_<Label, S, X>,
+    ),
+    IfBranchMustBeTerm(
+        bool,
+        Expr_<Label, S, X>,
+        Expr_<Label, S, X>,
+        Expr_<Label, 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>),
+    InvalidField(String, Expr_<Label, S, X>),
+    InvalidFieldType(String, Expr_<Label, S, X>),
+    InvalidAlternative(String, Expr_<Label, S, X>),
+    InvalidAlternativeType(String, Expr_<Label, S, X>),
     DuplicateAlternative(String),
-    MustCombineARecord(Expr<'i, S, X>, Expr<'i, S, X>),
+    MustCombineARecord(Expr_<Label, S, X>, Expr_<Label, S, X>),
     FieldCollision(String),
-    MustMergeARecord(Expr<'i, S, X>, Expr<'i, S, X>),
-    MustMergeUnion(Expr<'i, S, X>, Expr<'i, S, X>),
+    MustMergeARecord(Expr_<Label, S, X>, Expr_<Label, S, X>),
+    MustMergeUnion(Expr_<Label, S, X>, Expr_<Label, 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>),
+    HandlerInputTypeMismatch(String, Expr_<Label, S, X>, Expr_<Label, S, X>),
+    HandlerOutputTypeMismatch(String, Expr_<Label, S, X>, Expr_<Label, S, X>),
+    HandlerNotAFunction(String, Expr_<Label, S, X>),
+    NotARecord(String, Expr_<Label, S, X>, Expr_<Label, S, X>),
+    MissingField(String, Expr_<Label, S, X>),
+    CantAnd(Expr_<Label, S, X>, Expr_<Label, S, X>),
+    CantOr(Expr_<Label, S, X>, Expr_<Label, S, X>),
+    CantEQ(Expr_<Label, S, X>, Expr_<Label, S, X>),
+    CantNE(Expr_<Label, S, X>, Expr_<Label, S, X>),
+    CantTextAppend(Expr_<Label, S, X>, Expr_<Label, S, X>),
+    CantAdd(Expr_<Label, S, X>, Expr_<Label, S, X>),
+    CantMultiply(Expr_<Label, S, X>, Expr_<Label, S, X>),
+    NoDependentLet(Expr_<Label, S, X>, Expr_<Label, S, X>),
+    NoDependentTypes(Expr_<Label, S, X>, Expr_<Label, S, X>),
 }
 
 /// A structured type error that includes context
@@ -775,14 +789,14 @@ pub enum TypeMessage<'i, S> {
 pub struct TypeError<'i, S> {
     pub context: Context<&'i str, Expr<'i, S, X>>,
     pub current: Expr<'i, S, X>,
-    pub type_message: TypeMessage<'i, S>,
+    pub type_message: TypeMessage<&'i str, S>,
 }
 
 impl<'i, S: Clone> TypeError<'i, S> {
     pub fn new(
         context: &Context<&'i str, Expr<'i, S, X>>,
         current: &Expr<'i, S, X>,
-        type_message: TypeMessage<'i, S>,
+        type_message: TypeMessage<&'i str, S>,
     ) -> Self {
         TypeError {
             context: context.clone(),
@@ -792,7 +806,7 @@ impl<'i, S: Clone> TypeError<'i, S> {
     }
 }
 
-impl<'i, S: fmt::Debug> ::std::error::Error for TypeMessage<'i, S> {
+impl<'i, S: fmt::Debug> ::std::error::Error for TypeMessage<&'i str, S> {
     fn description(&self) -> &str {
         match *self {
             UnboundVariable => "Unbound variable",
@@ -805,7 +819,7 @@ impl<'i, S: fmt::Debug> ::std::error::Error for TypeMessage<'i, S> {
     }
 }
 
-impl<'i, S> fmt::Display for TypeMessage<'i, S> {
+impl<'i, S> fmt::Display for TypeMessage<&'i str, S> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         match *self {
             UnboundVariable => {