From bd1eb36503aa6e03532fefcfd0c4f27eb62c99d2 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 24 Jan 2020 16:29:25 +0000
Subject: Restore all types in Value::to_tyexpr

---
 dhall/src/semantics/phase/normalize.rs | 18 +++++++++++++-----
 dhall/src/semantics/phase/typecheck.rs | 12 +++++++-----
 2 files changed, 20 insertions(+), 10 deletions(-)

(limited to 'dhall/src/semantics/phase')

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);
-- 
cgit v1.2.3