Fix more bugs

5 files changed, 59 insertions, 65 deletions

diff --git a/dhall/build.rs b/dhall/build.rs
index c95a26d..cc94f5e 100644
--- a/dhall/build.rs
+++ b/dhall/build.rs
@@ -339,6 +339,8 @@ fn generate_tests() -> std::io::Result<()> {
                     || path == "unit/CompletionWithWrongDefaultType"
                     || path == "unit/CompletionWithWrongFieldName"
                     || path == "unit/CompletionWithWrongOverridenType"
+                    // TODO: enable free variable checking
+                    || path == "unit/MergeHandlerFreeVar"
             }),
             input_type: FileType::Text,
             output_type: None,
@@ -367,6 +369,8 @@ fn generate_tests() -> std::io::Result<()> {
                     || path == "unit/CompletionWithWrongDefaultType"
                     || path == "unit/CompletionWithWrongFieldName"
                     || path == "unit/CompletionWithWrongOverridenType"
+                    // TODO: enable free variable checking
+                    || path == "unit/MergeHandlerFreeVar"
             }),
             input_type: FileType::Text,
             output_type: None,
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index 532dae3..f4e4099 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -2,7 +2,7 @@
 use std::collections::HashMap;
 use std::convert::TryInto;
 
-use crate::semantics::nze::{NzVar, QuoteEnv};
+use crate::semantics::nze::NzVar;
 use crate::semantics::phase::typecheck::{
     builtin_to_value_env, const_to_value, rc,
 };
@@ -855,30 +855,14 @@ pub(crate) enum NzEnvItem {
 #[derive(Debug, Clone)]
 pub(crate) struct NzEnv {
     items: Vec<NzEnvItem>,
-    vars: QuoteEnv,
 }
 
 impl NzEnv {
     pub fn new() -> Self {
-        NzEnv {
-            items: Vec::new(),
-            vars: QuoteEnv::new(),
-        }
+        NzEnv { items: Vec::new() }
     }
     pub fn construct(items: Vec<NzEnvItem>) -> Self {
-        let vars = QuoteEnv::construct(
-            items
-                .iter()
-                .filter(|i| match i {
-                    NzEnvItem::Kept(_) => true,
-                    NzEnvItem::Replaced(_) => false,
-                })
-                .count(),
-        );
-        NzEnv { items, vars }
-    }
-    pub fn as_quoteenv(&self) -> QuoteEnv {
-        self.vars
+        NzEnv { items }
     }
     pub fn to_alpha_tyenv(&self) -> TyEnv {
         TyEnv::from_nzenv_alpha(self)
@@ -887,7 +871,6 @@ impl NzEnv {
     pub fn insert_type(&self, t: Value) -> Self {
         let mut env = self.clone();
         env.items.push(NzEnvItem::Kept(t));
-        env.vars = env.vars.insert();
         env
     }
     pub fn insert_value(&self, e: Value) -> Self {
@@ -897,16 +880,9 @@ impl NzEnv {
     }
     pub fn lookup_val(&self, var: &AlphaVar) -> Value {
         let idx = self.items.len() - 1 - var.idx();
-        let var_idx = self.items[..idx]
-            .iter()
-            .filter(|i| match i {
-                NzEnvItem::Kept(_) => true,
-                NzEnvItem::Replaced(_) => false,
-            })
-            .count();
         match &self.items[idx] {
             NzEnvItem::Kept(ty) => Value::from_kind_and_type_whnf(
-                ValueKind::Var(var.clone(), NzVar::new(var_idx)),
+                ValueKind::Var(var.clone(), NzVar::new(idx)),
                 ty.clone(),
             ),
             NzEnvItem::Replaced(x) => x.clone(),
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 1b8f261..a83f175 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -44,7 +44,7 @@ impl TyEnv {
         }
     }
     pub fn as_quoteenv(&self) -> QuoteEnv {
-        self.items.as_quoteenv()
+        self.names.as_quoteenv()
     }
     pub fn as_nzenv(&self) -> &NzEnv {
         &self.items
@@ -70,9 +70,6 @@ impl TyEnv {
         let ty = self.items.lookup_val(&var).get_type().unwrap();
         Some((TyExprKind::Var(var), ty))
     }
-    pub fn size(&self) -> usize {
-        self.names.size()
-    }
 }
 
 fn type_of_recordtype<'a>(
@@ -312,33 +309,24 @@ fn type_one_layer(
             let tf = f.get_type()?;
             let tf_borrow = tf.as_whnf();
             match &*tf_borrow {
-                // ValueKind::PiClosure { annot, closure, .. } => (annot, closure),
-                ValueKind::PiClosure {
-                    annot: _expected_arg_ty,
-                    closure: ty_closure,
-                    ..
-                } => {
-                    // if arg.get_type()? != *expected_arg_ty {
-                    //     return mkerr(format!(
-                    //         "function annot mismatch: {:?}, {:?}",
-                    //         arg.get_type()?,
-                    //         expected_arg_ty
-                    //     ));
-                    // }
+                ValueKind::PiClosure { annot, closure, .. } => {
+                    if arg.get_type()? != *annot {
+                        // return mkerr(format!("function annot mismatch"));
+                        return mkerr(format!(
+                            "function annot mismatch: ({} : {}) : {}",
+                            arg.to_expr_tyenv(env),
+                            arg.get_type()?
+                                .to_tyexpr(env.as_quoteenv())
+                                .to_expr_tyenv(env),
+                            annot
+                                .to_tyexpr(env.as_quoteenv())
+                                .to_expr_tyenv(env),
+                        ));
+                    }
 
                     let arg_nf = arg.normalize_whnf(env.as_nzenv());
-                    ty_closure.apply(arg_nf)
+                    closure.apply(arg_nf)
                 }
-                // ValueKind::Pi(_, _expected_arg_ty, body) => {
-                //     // if arg.get_type()? != *tx {
-                //     //     return mkerr("TypeMismatch");
-                //     // }
-
-                //     let arg_nf = arg.normalize_whnf(env.as_nzenv());
-                //     let ret = body.subst_shift(&AlphaVar::default(), &arg_nf);
-                //     ret.normalize_nf();
-                //     ret
-                // }
                 _ => return mkerr(format!("apply to not Pi: {:?}", tf_borrow)),
             }
         }
@@ -404,14 +392,29 @@ fn type_one_layer(
         ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => {
             let x_val = x.normalize_whnf(env.as_nzenv());
             let y_val = y.normalize_whnf(env.as_nzenv());
-            match &*x_val.as_whnf() {
-                ValueKind::RecordType(_) => {}
+            let x_val_borrow = x_val.as_whnf();
+            let y_val_borrow = y_val.as_whnf();
+            let kts_x = match &*x_val_borrow {
+                ValueKind::RecordType(kts) => kts,
                 _ => return mkerr("RecordTypeMergeRequiresRecordType"),
-            }
-            match &*y_val.as_whnf() {
-                ValueKind::RecordType(_) => {}
+            };
+            let kts_y = match &*y_val_borrow {
+                ValueKind::RecordType(kts) => kts,
                 _ => return mkerr("RecordTypeMergeRequiresRecordType"),
+            };
+            for (k, tx) in kts_x {
+                if let Some(ty) = kts_y.get(k) {
+                    type_one_layer(
+                        env,
+                        &ExprKind::BinOp(
+                            BinOp::RecursiveRecordTypeMerge,
+                            tx.to_tyexpr(env.as_quoteenv()),
+                            ty.to_tyexpr(env.as_quoteenv()),
+                        ),
+                    )?;
+                }
             }
+
             // A RecordType's type is always a const
             let xk = x.get_type()?.as_const().unwrap();
             let yk = y.get_type()?.as_const().unwrap();
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index 971c48d..1c687f6 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -193,13 +193,23 @@ pub fn run_test(test: Test<'_>) -> Result<()> {
             // assert_eq_pretty!(ty, expected);
         }
         TypeInferenceFailure(file_path) => {
-            let mut res =
-                parse_file_str(&file_path)?.skip_resolve()?.typecheck();
+            // let mut res =
+            //     parse_file_str(&file_path)?.skip_resolve()?.typecheck();
+            // if let Ok(e) = &res {
+            //     // If e did typecheck, check that get_type fails
+            //     res = e.get_type();
+            // }
+            // res.unwrap_err();
+
+            let res = crate::semantics::tck::typecheck::typecheck(
+                &parse_file_str(&file_path)?.skip_resolve()?.to_expr(),
+            );
             if let Ok(e) = &res {
                 // If e did typecheck, check that get_type fails
-                res = e.get_type();
+                e.get_type().unwrap_err();
+            } else {
+                res.unwrap_err();
             }
-            res.unwrap_err();
         }
         // Checks the output of the type error against a text file. If the text file doesn't exist,
         // we instead write to it the output we got. This makes it easy to update those files: just
diff --git a/tests_buffer b/tests_buffer
index e5e1705..34210a9 100644
--- a/tests_buffer
+++ b/tests_buffer
@@ -49,6 +49,7 @@ success/
         somehow test types added to the Foo/build closures
             λ(x : ∀(a : Type) → a) → x
             let X = 0 in λ(T : Type) → λ(x : T) → 1
+            (λ(T : Type) → let foo = 0 in λ(x : T) → x) : ∀(T : Type) → ∀(x : T) → T
 failure/
     merge { x = λ(x : Bool) → x } (< x: Bool | y: Natural >.x True)
     merge { x = λ(_ : Bool) → _, y = 1 } < x = True | y >