Restore all types in Value::to_tyexpr

4 files changed, 101 insertions, 64 deletions

diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index 8beed24..3798053 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -75,7 +75,8 @@ pub(crate) enum ValueKind<Value> {
         closure: Closure,
     },
     // Invariant: in whnf, the evaluation must not be able to progress further.
-    AppliedBuiltin(Builtin, Vec<Value>),
+    // Keep types around to be able to recover the types of partial applications.
+    AppliedBuiltin(Builtin, Vec<Value>, Vec<Value>),
 
     Var(AlphaVar, NzVar),
     Const(Const),
@@ -92,9 +93,9 @@ pub(crate) enum ValueKind<Value> {
     RecordLit(HashMap<Label, Value>),
     UnionType(HashMap<Label, Option<Value>>),
     // Also keep the type of the uniontype around
-    UnionConstructor(Label, HashMap<Label, Option<Value>>, Type),
+    UnionConstructor(Label, HashMap<Label, Option<Value>>, Value),
     // Also keep the type of the uniontype and the constructor around
-    UnionLit(Label, Value, HashMap<Label, Option<Value>>, Type, Type),
+    UnionLit(Label, Value, HashMap<Label, Option<Value>>, Value, Value),
     // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and
     // contiguous text values must be merged.
     TextLit(Vec<InterpolatedTextContents<Value>>),
@@ -309,8 +310,68 @@ impl Value {
                 annot.to_tyexpr(qenv),
                 closure.apply_ty(annot.clone()).to_tyexpr(qenv.insert()),
             )),
+            ValueKind::AppliedBuiltin(b, args, types) => {
+                TyExprKind::Expr(args.into_iter().zip(types.into_iter()).fold(
+                    ExprKind::Builtin(*b),
+                    |acc, (v, ty)| {
+                        ExprKind::App(
+                            TyExpr::new(
+                                TyExprKind::Expr(acc),
+                                Some(ty.clone()),
+                                Span::Artificial,
+                            ),
+                            v.to_tyexpr(qenv),
+                        )
+                    },
+                ))
+            }
+            ValueKind::UnionConstructor(l, kts, t) => {
+                TyExprKind::Expr(ExprKind::Field(
+                    TyExpr::new(
+                        TyExprKind::Expr(ExprKind::UnionType(
+                            kts.into_iter()
+                                .map(|(k, v)| {
+                                    (
+                                        k.clone(),
+                                        v.as_ref().map(|v| v.to_tyexpr(qenv)),
+                                    )
+                                })
+                                .collect(),
+                        )),
+                        Some(t.clone()),
+                        Span::Artificial,
+                    ),
+                    l.clone(),
+                ))
+            }
+            ValueKind::UnionLit(l, v, kts, uniont, ctort) => {
+                TyExprKind::Expr(ExprKind::App(
+                    TyExpr::new(
+                        TyExprKind::Expr(ExprKind::Field(
+                            TyExpr::new(
+                                TyExprKind::Expr(ExprKind::UnionType(
+                                    kts.into_iter()
+                                        .map(|(k, v)| {
+                                            (
+                                                k.clone(),
+                                                v.as_ref()
+                                                    .map(|v| v.to_tyexpr(qenv)),
+                                            )
+                                        })
+                                        .collect(),
+                                )),
+                                Some(uniont.clone()),
+                                Span::Artificial,
+                            ),
+                            l.clone(),
+                        )),
+                        Some(ctort.clone()),
+                        Span::Artificial,
+                    ),
+                    v.to_tyexpr(qenv),
+                ))
+            }
             self_kind => {
-                // TODO: properly recover intermediate types; `None` is a time-bomb here.
                 let self_kind = self_kind
                     .map_ref_with_special_handling_of_binders(
                         |v| v.to_tyexpr(qenv),
@@ -319,23 +380,14 @@ impl Value {
                 let expr = match self_kind {
                     ValueKind::Var(..)
                     | ValueKind::LamClosure { .. }
-                    | ValueKind::PiClosure { .. } => unreachable!(),
+                    | ValueKind::PiClosure { .. }
+                    | ValueKind::AppliedBuiltin(..)
+                    | ValueKind::UnionConstructor(..)
+                    | ValueKind::UnionLit(..) => unreachable!(),
                     ValueKind::Lam(x, t, e) => {
                         ExprKind::Lam(x.to_label(), t, e)
                     }
                     ValueKind::Pi(x, t, e) => ExprKind::Pi(x.to_label(), t, e),
-                    ValueKind::AppliedBuiltin(b, args) => {
-                        args.into_iter().fold(ExprKind::Builtin(b), |acc, v| {
-                            ExprKind::App(
-                                TyExpr::new(
-                                    TyExprKind::Expr(acc),
-                                    None, // TODO
-                                    Span::Artificial,
-                                ),
-                                v,
-                            )
-                        })
-                    }
                     ValueKind::Const(c) => ExprKind::Const(c),
                     ValueKind::BoolLit(b) => ExprKind::BoolLit(b),
                     ValueKind::NaturalLit(n) => ExprKind::NaturalLit(n),
@@ -366,35 +418,6 @@ impl Value {
                     ValueKind::UnionType(kts) => {
                         ExprKind::UnionType(kts.into_iter().collect())
                     }
-                    ValueKind::UnionConstructor(l, kts, t) => ExprKind::Field(
-                        TyExpr::new(
-                            TyExprKind::Expr(ExprKind::UnionType(
-                                kts.into_iter().collect(),
-                            )),
-                            Some(t),
-                            Span::Artificial,
-                        ),
-                        l,
-                    ),
-                    ValueKind::UnionLit(l, v, kts, uniont, ctort) => {
-                        ExprKind::App(
-                            TyExpr::new(
-                                TyExprKind::Expr(ExprKind::Field(
-                                    TyExpr::new(
-                                        TyExprKind::Expr(ExprKind::UnionType(
-                                            kts.into_iter().collect(),
-                                        )),
-                                        Some(uniont),
-                                        Span::Artificial,
-                                    ),
-                                    l,
-                                )),
-                                Some(ctort),
-                                Span::Artificial,
-                            ),
-                            v,
-                        )
-                    }
                     ValueKind::TextLit(elts) => {
                         ExprKind::TextLit(elts.into_iter().collect())
                     }
@@ -530,7 +553,7 @@ impl ValueKind<Value> {
             | ValueKind::PiClosure { annot, .. } => {
                 annot.normalize_mut();
             }
-            ValueKind::AppliedBuiltin(_, args) => {
+            ValueKind::AppliedBuiltin(_, args, _) => {
                 for x in args.iter_mut() {
                     x.normalize_mut();
                 }
@@ -578,7 +601,7 @@ impl ValueKind<Value> {
     }
 
     pub(crate) fn from_builtin(b: Builtin) -> ValueKind<Value> {
-        ValueKind::AppliedBuiltin(b, vec![])
+        ValueKind::AppliedBuiltin(b, vec![], vec![])
     }
 
     fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
diff --git a/dhall/src/semantics/core/visitor.rs b/dhall/src/semantics/core/visitor.rs
index ee44ed7..64250b0 100644
--- a/dhall/src/semantics/core/visitor.rs
+++ b/dhall/src/semantics/core/visitor.rs
@@ -98,7 +98,9 @@ where
             annot: v.visit_val(annot)?,
             closure: closure.clone(),
         },
-        AppliedBuiltin(b, xs) => AppliedBuiltin(*b, v.visit_vec(xs)?),
+        AppliedBuiltin(b, xs, types) => {
+            AppliedBuiltin(*b, v.visit_vec(xs)?, v.visit_vec(types)?)
+        }
         Var(v, w) => Var(v.clone(), *w),
         Const(k) => Const(*k),
         BoolLit(b) => BoolLit(*b),
@@ -112,15 +114,17 @@ where
         RecordType(kts) => RecordType(v.visit_map(kts)?),
         RecordLit(kvs) => RecordLit(v.visit_map(kvs)?),
         UnionType(kts) => UnionType(v.visit_optmap(kts)?),
-        UnionConstructor(l, kts, t) => {
-            UnionConstructor(l.clone(), v.visit_optmap(kts)?, t.clone())
-        }
+        UnionConstructor(l, kts, uniont) => UnionConstructor(
+            l.clone(),
+            v.visit_optmap(kts)?,
+            v.visit_val(uniont)?,
+        ),
         UnionLit(l, x, kts, uniont, ctort) => UnionLit(
             l.clone(),
             v.visit_val(x)?,
             v.visit_optmap(kts)?,
-            uniont.clone(),
-            ctort.clone(),
+            v.visit_val(uniont)?,
+            v.visit_val(ctort)?,
         ),
         TextLit(ts) => TextLit(
             ts.iter()
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index 75d61d5..8f3953d 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -71,6 +71,7 @@ pub(crate) fn apply_builtin(
     b: Builtin,
     args: Vec<Value>,
     ty: &Value,
+    types: Vec<Value>,
 ) -> ValueKind<Value> {
     use syntax::Builtin::*;
     use ValueKind::*;
@@ -364,7 +365,7 @@ pub(crate) fn apply_builtin(
             }
             v.to_whnf_check_type(ty)
         }
-        Ret::DoneAsIs => AppliedBuiltin(b, args),
+        Ret::DoneAsIs => AppliedBuiltin(b, args, types),
     }
 }
 
@@ -377,10 +378,15 @@ pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind<Value> {
         ValueKind::LamClosure { closure, .. } => {
             closure.apply(a).to_whnf_check_type(ty)
         }
-        ValueKind::AppliedBuiltin(b, args) => {
+        ValueKind::AppliedBuiltin(b, args, types) => {
             use std::iter::once;
             let args = args.iter().cloned().chain(once(a.clone())).collect();
-            apply_builtin(*b, args, ty)
+            let types = types
+                .iter()
+                .cloned()
+                .chain(once(f.get_type().unwrap()))
+                .collect();
+            apply_builtin(*b, args, ty, types)
         }
         ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit(
             l.clone(),
@@ -631,7 +637,7 @@ pub(crate) fn normalize_one_layer(
         ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)),
         ExprKind::EmptyListLit(t) => {
             let arg = match &*t.as_whnf() {
-                ValueKind::AppliedBuiltin(syntax::Builtin::List, args)
+                ValueKind::AppliedBuiltin(syntax::Builtin::List, args, _)
                     if args.len() == 1 =>
                 {
                     args[0].clone()
@@ -806,7 +812,9 @@ pub(crate) fn normalize_whnf(
     ty: &Value,
 ) -> ValueKind<Value> {
     match v {
-        ValueKind::AppliedBuiltin(b, args) => apply_builtin(b, args, ty),
+        ValueKind::AppliedBuiltin(b, args, types) => {
+            apply_builtin(b, args, ty, types)
+        }
         ValueKind::PartialExpr(e) => normalize_one_layer(e, ty),
         ValueKind::TextLit(elts) => {
             ValueKind::TextLit(squash_textlit(elts.into_iter()))
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index 9e41f1e..f2d1bf2 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -421,7 +421,7 @@ fn type_last_layer(
         }
         EmptyListLit(t) => {
             let arg = match &*t.as_whnf() {
-                ValueKind::AppliedBuiltin(syntax::Builtin::List, args)
+                ValueKind::AppliedBuiltin(syntax::Builtin::List, args, _)
                     if args.len() == 1 =>
                 {
                     args[0].clone()
@@ -613,7 +613,7 @@ fn type_last_layer(
         }
         BinOp(o @ ListAppend, l, r) => {
             match &*l.get_type()?.as_whnf() {
-                ValueKind::AppliedBuiltin(List, _) => {}
+                ValueKind::AppliedBuiltin(List, _, _) => {}
                 _ => return mkerr(BinOpTypeMismatch(*o, l.clone())),
             }
 
@@ -679,9 +679,11 @@ fn type_last_layer(
             let union_borrow = union_type.as_whnf();
             let variants = match &*union_borrow {
                 ValueKind::UnionType(kts) => Cow::Borrowed(kts),
-                ValueKind::AppliedBuiltin(syntax::Builtin::Optional, args)
-                    if args.len() == 1 =>
-                {
+                ValueKind::AppliedBuiltin(
+                    syntax::Builtin::Optional,
+                    args,
+                    _,
+                ) if args.len() == 1 => {
                     let ty = &args[0];
                     let mut kts = HashMap::new();
                     kts.insert("None".into(), None);