More typecheck

3 files changed, 301 insertions, 58 deletions

diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index 7f547d7..33e1f2b 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -595,8 +595,23 @@ fn apply_binop<'a>(
             Ret::ValueKind(RecordLit(kvs))
         }
 
-        (RecursiveRecordTypeMerge, _, _) => {
-            unreachable!("This case should have been handled in typecheck")
+        (RecursiveRecordTypeMerge, RecordType(kts_x), RecordType(kts_y)) => {
+            let kts = merge_maps::<_, _, _, !>(
+                kts_x,
+                kts_y,
+                // If the Label exists for both records, then we hit the recursive case.
+                |_, l: &Value, r: &Value| {
+                    Ok(Value::from_kind_and_type(
+                        ValueKind::PartialExpr(ExprKind::BinOp(
+                            RecursiveRecordTypeMerge,
+                            l.clone(),
+                            r.clone(),
+                        )),
+                        ty.clone(),
+                    ))
+                },
+            )?;
+            Ret::ValueKind(RecordType(kts))
         }
 
         (Equivalence, _, _) => {
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index 44678cd..1aab736 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -356,7 +356,6 @@ fn type_last_layer(
     use syntax::BinOp::*;
     use syntax::Builtin::*;
     use syntax::Const::Type;
-    use syntax::ExprKind::*;
     let mkerr =
         |msg: &str| Err(TypeError::new(TypeMessage::Custom(msg.to_string())));
 
@@ -370,13 +369,15 @@ fn type_last_layer(
     use Ret::*;
 
     let ret = match &e {
-        Import(_) => unreachable!(
+        ExprKind::Import(_) => unreachable!(
             "There should remain no imports in a resolved expression"
         ),
-        Lam(_, _, _) | Pi(_, _, _) | Let(_, _, _, _) | Embed(_) | Var(_) => {
-            unreachable!()
-        }
-        App(f, a) => {
+        ExprKind::Lam(_, _, _)
+        | ExprKind::Pi(_, _, _)
+        | ExprKind::Let(_, _, _, _)
+        | ExprKind::Embed(_)
+        | ExprKind::Var(_) => unreachable!(),
+        ExprKind::App(f, a) => {
             let tf = f.get_type()?;
             let tf_borrow = tf.as_whnf();
             let (tx, tb) = match &*tf_borrow {
@@ -391,13 +392,13 @@ fn type_last_layer(
             ret.normalize_nf();
             RetTypeOnly(ret)
         }
-        Annot(x, t) => {
+        ExprKind::Annot(x, t) => {
             if &x.get_type()? != t {
                 return mkerr("AnnotMismatch");
             }
             RetWhole(x.clone())
         }
-        Assert(t) => {
+        ExprKind::Assert(t) => {
             match &*t.as_whnf() {
                 ValueKind::Equivalence(x, y) if x == y => {}
                 ValueKind::Equivalence(..) => return mkerr("AssertMismatch"),
@@ -405,16 +406,16 @@ fn type_last_layer(
             }
             RetTypeOnly(t.clone())
         }
-        BoolIf(x, y, z) => {
+        ExprKind::BoolIf(x, y, z) => {
             if *x.get_type()?.as_whnf() != ValueKind::from_builtin(Bool) {
                 return mkerr("InvalidPredicate");
             }
 
-            if y.get_type()?.get_type()?.as_const() != Some(Type) {
+            if y.get_type()?.get_type()?.as_const() != Some(Const::Type) {
                 return mkerr("IfBranchMustBeTerm");
             }
 
-            if z.get_type()?.get_type()?.as_const() != Some(Type) {
+            if z.get_type()?.get_type()?.as_const() != Some(Const::Type) {
                 return mkerr("IfBranchMustBeTerm");
             }
 
@@ -424,7 +425,7 @@ fn type_last_layer(
 
             RetTypeOnly(y.get_type()?)
         }
-        EmptyListLit(t) => {
+        ExprKind::EmptyListLit(t) => {
             let arg = match &*t.as_whnf() {
                 ValueKind::AppliedBuiltin(syntax::Builtin::List, args, _)
                     if args.len() == 1 =>
@@ -438,7 +439,7 @@ fn type_last_layer(
                 t.clone(),
             ))
         }
-        NEListLit(xs) => {
+        ExprKind::NEListLit(xs) => {
             let mut iter = xs.iter().enumerate();
             let (_, x) = iter.next().unwrap();
             for (_, y) in iter {
@@ -447,30 +448,30 @@ fn type_last_layer(
                 }
             }
             let t = x.get_type()?;
-            if t.get_type()?.as_const() != Some(Type) {
+            if t.get_type()?.as_const() != Some(Const::Type) {
                 return mkerr("InvalidListType");
             }
 
             RetTypeOnly(Value::from_builtin(syntax::Builtin::List).app(t))
         }
-        SomeLit(x) => {
+        ExprKind::SomeLit(x) => {
             let t = x.get_type()?;
-            if t.get_type()?.as_const() != Some(Type) {
+            if t.get_type()?.as_const() != Some(Const::Type) {
                 return mkerr("InvalidOptionalType");
             }
 
             RetTypeOnly(Value::from_builtin(syntax::Builtin::Optional).app(t))
         }
-        RecordType(kts) => RetWhole(tck_record_type(
+        ExprKind::RecordType(kts) => RetWhole(tck_record_type(
             kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))),
         )?),
-        UnionType(kts) => RetWhole(tck_union_type(
+        ExprKind::UnionType(kts) => RetWhole(tck_union_type(
             kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))),
         )?),
-        RecordLit(kvs) => RetTypeOnly(tck_record_type(
+        ExprKind::RecordLit(kvs) => RetTypeOnly(tck_record_type(
             kvs.iter().map(|(x, v)| Ok((x.clone(), v.get_type()?))),
         )?),
-        Field(r, x) => {
+        ExprKind::Field(r, x) => {
             match &*r.get_type()?.as_whnf() {
                 ValueKind::RecordType(kts) => match kts.get(&x) {
                     Some(tth) => RetTypeOnly(tth.clone()),
@@ -494,13 +495,13 @@ fn type_last_layer(
                 } // _ => mkerr("NotARecord"),
             }
         }
-        Const(c) => RetWhole(const_to_value(*c)),
-        Builtin(b) => RetWhole(builtin_to_value(*b)),
-        BoolLit(_) => RetTypeOnly(builtin_to_value(Bool)),
-        NaturalLit(_) => RetTypeOnly(builtin_to_value(Natural)),
-        IntegerLit(_) => RetTypeOnly(builtin_to_value(Integer)),
-        DoubleLit(_) => RetTypeOnly(builtin_to_value(Double)),
-        TextLit(interpolated) => {
+        ExprKind::Const(c) => RetWhole(const_to_value(*c)),
+        ExprKind::Builtin(b) => RetWhole(builtin_to_value(*b)),
+        ExprKind::BoolLit(_) => RetTypeOnly(builtin_to_value(Bool)),
+        ExprKind::NaturalLit(_) => RetTypeOnly(builtin_to_value(Natural)),
+        ExprKind::IntegerLit(_) => RetTypeOnly(builtin_to_value(Integer)),
+        ExprKind::DoubleLit(_) => RetTypeOnly(builtin_to_value(Double)),
+        ExprKind::TextLit(interpolated) => {
             let text_type = builtin_to_value(Text);
             for contents in interpolated.iter() {
                 use InterpolatedTextContents::Expr;
@@ -512,7 +513,7 @@ fn type_last_layer(
             }
             RetTypeOnly(text_type)
         }
-        BinOp(RightBiasedRecordMerge, l, r) => {
+        ExprKind::BinOp(RightBiasedRecordMerge, l, r) => {
             let l_type = l.get_type()?;
             let r_type = r.get_type()?;
 
@@ -541,16 +542,18 @@ fn type_last_layer(
                 kts.into_iter().map(|(x, v)| Ok((x.clone(), v))),
             )?)
         }
-        BinOp(RecursiveRecordMerge, l, r) => RetTypeOnly(type_last_layer(
-            ctx,
-            ExprKind::BinOp(
-                RecursiveRecordTypeMerge,
-                l.get_type()?,
-                r.get_type()?,
-            ),
-            Span::Artificial,
-        )?),
-        BinOp(RecursiveRecordTypeMerge, l, r) => {
+        ExprKind::BinOp(RecursiveRecordMerge, l, r) => {
+            RetTypeOnly(type_last_layer(
+                ctx,
+                ExprKind::BinOp(
+                    RecursiveRecordTypeMerge,
+                    l.get_type()?,
+                    r.get_type()?,
+                ),
+                Span::Artificial,
+            )?)
+        }
+        ExprKind::BinOp(RecursiveRecordTypeMerge, l, r) => {
             // Extract the LHS record type
             let borrow_l = l.as_whnf();
             let kts_x = match &*borrow_l {
@@ -585,7 +588,7 @@ fn type_last_layer(
 
             RetWhole(tck_record_type(kts.into_iter().map(Ok))?)
         }
-        BinOp(ListAppend, l, r) => {
+        ExprKind::BinOp(ListAppend, l, r) => {
             match &*l.get_type()?.as_whnf() {
                 ValueKind::AppliedBuiltin(List, _, _) => {}
                 _ => return mkerr("BinOpTypeMismatch"),
@@ -597,11 +600,11 @@ fn type_last_layer(
 
             RetTypeOnly(l.get_type()?)
         }
-        BinOp(Equivalence, l, r) => {
-            if l.get_type()?.get_type()?.as_const() != Some(Type) {
+        ExprKind::BinOp(Equivalence, l, r) => {
+            if l.get_type()?.get_type()?.as_const() != Some(Const::Type) {
                 return mkerr("EquivalenceArgumentMustBeTerm");
             }
-            if r.get_type()?.get_type()?.as_const() != Some(Type) {
+            if r.get_type()?.get_type()?.as_const() != Some(Const::Type) {
                 return mkerr("EquivalenceArgumentMustBeTerm");
             }
 
@@ -614,7 +617,7 @@ fn type_last_layer(
                 Value::from_const(Type),
             ))
         }
-        BinOp(o, l, r) => {
+        ExprKind::BinOp(o, l, r) => {
             let t = builtin_to_value(match o {
                 BoolAnd => Bool,
                 BoolOr => Bool,
@@ -641,7 +644,7 @@ fn type_last_layer(
 
             RetTypeOnly(t)
         }
-        Merge(record, union, type_annot) => {
+        ExprKind::Merge(record, union, type_annot) => {
             let record_type = record.get_type()?;
             let record_borrow = record_type.as_whnf();
             let handlers = match &*record_borrow {
@@ -723,8 +726,8 @@ fn type_last_layer(
                 (None, None) => return mkerr("MergeEmptyNeedsAnnotation"),
             }
         }
-        ToMap(_, _) => unimplemented!("toMap"),
-        Projection(record, labels) => {
+        ExprKind::ToMap(_, _) => unimplemented!("toMap"),
+        ExprKind::Projection(record, labels) => {
             let record_type = record.get_type()?;
             let record_type_borrow = record_type.as_whnf();
             let kts = match &*record_type_borrow {
@@ -753,8 +756,10 @@ fn type_last_layer(
                 record_type.get_type()?,
             ))
         }
-        ProjectionByExpr(_, _) => unimplemented!("selection by expression"),
-        Completion(_, _) => unimplemented!("record completion"),
+        ExprKind::ProjectionByExpr(_, _) => {
+            unimplemented!("selection by expression")
+        }
+        ExprKind::Completion(_, _) => unimplemented!("record completion"),
     };
 
     Ok(match ret {
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 52c7ac7..1687185 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -19,8 +19,8 @@ use crate::semantics::{
 };
 use crate::syntax;
 use crate::syntax::{
-    Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, Span,
-    UnspannedExpr, V,
+    BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label,
+    Span, UnspannedExpr, V,
 };
 
 #[derive(Debug, Clone)]
@@ -46,7 +46,7 @@ impl TyEnv {
         &self.names
     }
 
-    pub fn insert_type(&self, x: &Label, t: Value) -> Self {
+    pub fn insert_type(&self, x: &Label, t: Type) -> Self {
         TyEnv {
             names: self.names.insert(x),
             items: self.items.insert_type(t),
@@ -58,7 +58,7 @@ impl TyEnv {
             items: self.items.insert_value(e),
         }
     }
-    pub fn lookup(&self, var: &V<Label>) -> Option<(TyExprKind, Value)> {
+    pub fn lookup(&self, var: &V<Label>) -> Option<(TyExprKind, Type)> {
         let var = self.names.unlabel_var(var)?;
         let ty = self.items.lookup_val(&var).get_type().unwrap();
         Some((TyExprKind::Var(var), ty))
@@ -72,10 +72,10 @@ fn mkerr<T>(x: impl ToString) -> Result<T, TypeError> {
     Err(TypeError::new(TypeMessage::Custom(x.to_string())))
 }
 
-fn type_last_layer(
+fn type_one_layer(
     env: &TyEnv,
     kind: &ExprKind<TyExpr, Normalized>,
-) -> Result<Value, TypeError> {
+) -> Result<Type, TypeError> {
     Ok(match &kind {
         ExprKind::Import(..) => unreachable!(
             "There should remain no imports in a resolved expression"
@@ -85,7 +85,7 @@ fn type_last_layer(
         | ExprKind::Pi(..)
         | ExprKind::Let(..)
         | ExprKind::Const(Const::Sort)
-        | ExprKind::Embed(..) => unreachable!(),
+        | ExprKind::Embed(..) => unreachable!(), // Handled in type_with
 
         ExprKind::Const(Const::Type) => const_to_value(Const::Kind),
         ExprKind::Const(Const::Kind) => const_to_value(Const::Sort),
@@ -96,7 +96,99 @@ fn type_last_layer(
         ExprKind::NaturalLit(_) => builtin_to_value(Builtin::Natural),
         ExprKind::IntegerLit(_) => builtin_to_value(Builtin::Integer),
         ExprKind::DoubleLit(_) => builtin_to_value(Builtin::Double),
+        ExprKind::TextLit(interpolated) => {
+            let text_type = builtin_to_value(Builtin::Text);
+            for contents in interpolated.iter() {
+                use InterpolatedTextContents::Expr;
+                if let Expr(x) = contents {
+                    if x.get_type()? != text_type {
+                        return mkerr("InvalidTextInterpolation");
+                    }
+                }
+            }
+            text_type
+        }
+
+        // ExprKind::EmptyListLit(t) => {
+        //     let arg = match &*t.as_whnf() {
+        //         ValueKind::AppliedBuiltin(Builtin::List, args, _)
+        //             if args.len() == 1 =>
+        //         {
+        //             args[0].clone()
+        //         }
+        //         _ => return mkerr("InvalidListType"),
+        //     };
+        //     RetWhole(Value::from_kind_and_type(
+        //         ValueKind::EmptyListLit(arg),
+        //         t.clone(),
+        //     ))
+        // }
+        ExprKind::NEListLit(xs) => {
+            let mut iter = xs.iter().enumerate();
+            let (_, x) = iter.next().unwrap();
+            for (i, y) in iter {
+                if x.get_type()? != y.get_type()? {
+                    return mkerr("InvalidListElement");
+                }
+            }
+            let t = x.get_type()?;
+            if t.get_type()?.as_const() != Some(Const::Type) {
+                return mkerr("InvalidListType");
+            }
+
+            Value::from_builtin(Builtin::List).app(t)
+        }
+        ExprKind::SomeLit(x) => {
+            let t = x.get_type()?;
+            if t.get_type()?.as_const() != Some(Const::Type) {
+                return mkerr("InvalidOptionalType");
+            }
 
+            Value::from_builtin(Builtin::Optional).app(t)
+        }
+        // ExprKind::RecordType(kts) => RetWhole(tck_record_type(
+        //     kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))),
+        // )?),
+        // ExprKind::UnionType(kts) => RetWhole(tck_union_type(
+        //     kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))),
+        // )?),
+        // ExprKind::RecordLit(kvs) => RetTypeOnly(tck_record_type(
+        //     kvs.iter().map(|(x, v)| Ok((x.clone(), v.get_type()?))),
+        // )?),
+        ExprKind::Field(r, x) => {
+            match &*r.get_type()?.as_whnf() {
+                ValueKind::RecordType(kts) => match kts.get(&x) {
+                    Some(tth) => tth.clone(),
+                    None => return mkerr("MissingRecordField"),
+                },
+                // TODO: branch here only when r.get_type() is a Const
+                _ => {
+                    let r_nf = r.normalize_whnf(env.as_nzenv());
+                    let r_nf_borrow = r_nf.as_whnf();
+                    match &*r_nf_borrow {
+                        ValueKind::UnionType(kts) => match kts.get(x) {
+                            // Constructor has type T -> < x: T, ... >
+                            // TODO: check pi type properly
+                            Some(Some(t)) => Value::from_kind_and_type(
+                                ValueKind::PiClosure {
+                                    binder: Binder::new(x.clone()),
+                                    annot: t.clone(),
+                                    closure: Closure::new(
+                                        t.clone(),
+                                        env.as_nzenv(),
+                                        r.clone(),
+                                    ),
+                                },
+                                Value::from_const(Const::Type),
+                            ),
+                            Some(None) => r_nf.clone(),
+                            None => return mkerr("MissingUnionField"),
+                        },
+                        _ => return mkerr("NotARecord"),
+                    }
+                } // _ => mkerr("NotARecord"),
+            }
+        }
         ExprKind::Annot(x, t) => {
             if x.get_type()? != t.normalize_whnf(env.as_nzenv()) {
                 return mkerr("annot mismatch");
@@ -139,7 +231,138 @@ fn type_last_layer(
 
             y.get_type()?
         }
+        // ExprKind::BinOp(BinOp::RightBiasedRecordMerge, l, r) => {
+        //     let l_type = l.get_type()?;
+        //     let r_type = r.get_type()?;
+
+        //     // Extract the LHS record type
+        //     let l_type_borrow = l_type.as_whnf();
+        //     let kts_x = match &*l_type_borrow {
+        //         ValueKind::RecordType(kts) => kts,
+        //         _ => return mkerr("MustCombineRecord"),
+        //     };
+
+        //     // Extract the RHS record type
+        //     let r_type_borrow = r_type.as_whnf();
+        //     let kts_y = match &*r_type_borrow {
+        //         ValueKind::RecordType(kts) => kts,
+        //         _ => return mkerr("MustCombineRecord"),
+        //     };
 
+        //     // Union the two records, prefering
+        //     // the values found in the RHS.
+        //     let kts = merge_maps::<_, _, _, !>(kts_x, kts_y, |_, _, r_t| {
+        //         Ok(r_t.clone())
+        //     })?;
+
+        //     // Construct the final record type from the union
+        //     RetTypeOnly(tck_record_type(
+        //         kts.into_iter().map(|(x, v)| Ok((x.clone(), v))),
+        //     )?)
+        // }
+        // ExprKind::BinOp(BinOp::RecursiveRecordMerge, l, r) => RetTypeOnly(type_last_layer(
+        //     ctx,
+        //     ExprKind::BinOp(
+        //         RecursiveRecordTypeMerge,
+        //         l.get_type()?,
+        //         r.get_type()?,
+        //     ),
+        //     Span::Artificial,
+        // )?),
+        // ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, l, r) => {
+        //     // Extract the LHS record type
+        //     let borrow_l = l.as_whnf();
+        //     let kts_x = match &*borrow_l {
+        //         ValueKind::RecordType(kts) => kts,
+        //         _ => {
+        //             return mkerr("RecordTypeMergeRequiresRecordType")
+        //         }
+        //     };
+
+        //     // Extract the RHS record type
+        //     let borrow_r = r.as_whnf();
+        //     let kts_y = match &*borrow_r {
+        //         ValueKind::RecordType(kts) => kts,
+        //         _ => {
+        //             return mkerr("RecordTypeMergeRequiresRecordType")
+        //         }
+        //     };
+
+        //     // Ensure that the records combine without a type error
+        //     let kts = merge_maps(
+        //         kts_x,
+        //         kts_y,
+        //         // If the Label exists for both records, then we hit the recursive case.
+        //         |_, l: &Value, r: &Value| {
+        //             type_last_layer(
+        //                 ctx,
+        //                 ExprKind::BinOp(
+        //                     RecursiveRecordTypeMerge,
+        //                     l.clone(),
+        //                     r.clone(),
+        //                 ),
+        //                 Span::Artificial,
+        //             )
+        //         },
+        //     )?;
+
+        //     RetWhole(tck_record_type(kts.into_iter().map(Ok))?)
+        // }
+        // ExprKind::BinOp(o @ BinOp::ListAppend, l, r) => {
+        //     match &*l.get_type()?.as_whnf() {
+        //         ValueKind::AppliedBuiltin(List, _, _) => {}
+        //         _ => return mkerr("BinOpTypeMismatch"),
+        //     }
+
+        //     if l.get_type()? != r.get_type()? {
+        //         return mkerr("BinOpTypeMismatch");
+        //     }
+
+        //     l.get_type()?
+        // }
+        // ExprKind::BinOp(BinOp::Equivalence, l, r) => {
+        //     if l.get_type()?.get_type()?.as_const() != Some(Const::Type) {
+        //         return mkerr("EquivalenceArgumentMustBeTerm");
+        //     }
+        //     if r.get_type()?.get_type()?.as_const() != Some(Const::Type) {
+        //         return mkerr("EquivalenceArgumentMustBeTerm");
+        //     }
+
+        //     if l.get_type()? != r.get_type()? {
+        //         return mkerr("EquivalenceTypeMismatch");
+        //     }
+
+        //     RetWhole(Value::from_kind_and_type(
+        //         ValueKind::Equivalence(l.clone(), r.clone()),
+        //         Value::from_const(Type),
+        //     ))
+        // }
+        ExprKind::BinOp(o, l, r) => {
+            let t = builtin_to_value(match o {
+                BinOp::BoolAnd
+                | BinOp::BoolOr
+                | BinOp::BoolEQ
+                | BinOp::BoolNE => Builtin::Bool,
+                BinOp::NaturalPlus | BinOp::NaturalTimes => Builtin::Natural,
+                BinOp::TextAppend => Builtin::Text,
+                BinOp::ListAppend
+                | BinOp::RightBiasedRecordMerge
+                | BinOp::RecursiveRecordMerge
+                | BinOp::RecursiveRecordTypeMerge
+                | BinOp::Equivalence => unreachable!(),
+                BinOp::ImportAlt => unreachable!("ImportAlt leftover in tck"),
+            });
+
+            if l.get_type()? != t {
+                return mkerr("BinOpTypeMismatch");
+            }
+
+            if r.get_type()? != t {
+                return mkerr("BinOpTypeMismatch");
+            }
+
+            t
+        }
         _ => Value::from_const(Const::Type), // TODO
     })
 }
@@ -216,7 +439,7 @@ fn type_with(
         }
         ekind => {
             let ekind = ekind.traverse_ref(|e| type_with(env, e))?;
-            let ty = type_last_layer(env, &ekind)?;
+            let ty = type_one_layer(env, &ekind)?;
             (TyExprKind::Expr(ekind), Some(ty))
         }
     };