From f5a588defc0ad22ce2f0d3b32ef8f0e22e43e672 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 24 Dec 2019 21:46:29 +0000
Subject: Ensure inferred type is always in normal form

---
 dhall/src/semantics/phase/mod.rs       | 11 ++++++++++-
 dhall/src/semantics/phase/typecheck.rs |  5 ++++-
 2 files changed, 14 insertions(+), 2 deletions(-)

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

diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs
index b22120d..5332eb3 100644
--- a/dhall/src/semantics/phase/mod.rs
+++ b/dhall/src/semantics/phase/mod.rs
@@ -63,6 +63,11 @@ impl Parsed {
     pub fn encode(&self) -> Result<Vec<u8>, EncodeError> {
         binary::encode(&self.0)
     }
+
+    /// Converts a value back to the corresponding AST expression.
+    pub fn to_expr(&self) -> ParsedExpr {
+        self.0.clone()
+    }
 }
 
 impl Resolved {
@@ -73,6 +78,10 @@ impl Resolved {
         Ok(typecheck::typecheck_with(self.0, ty.normalize_to_expr())?
             .into_typed())
     }
+    /// Converts a value back to the corresponding AST expression.
+    pub fn to_expr(&self) -> ResolvedExpr {
+        self.0.clone()
+    }
 }
 
 impl Typed {
@@ -96,7 +105,7 @@ impl Typed {
     }
 
     /// Converts a value back to the corresponding AST expression.
-    pub(crate) fn to_expr(&self) -> NormalizedExpr {
+    pub fn to_expr(&self) -> ResolvedExpr {
         self.0.to_expr(ToExprOptions {
             alpha: false,
             normalize: false,
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index e9836e8..3960146 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -315,6 +315,7 @@ fn type_with(
     Ok(match e.as_ref() {
         Lam(var, annot, body) => {
             let annot = type_with(ctx, annot.clone())?;
+            annot.normalize_nf();
             let ctx2 = ctx.insert_type(var, annot.clone());
             let body = type_with(&ctx2, body.clone())?;
             let body_type = body.get_type()?;
@@ -401,7 +402,9 @@ fn type_last_layer(
                 return mkerr(TypeMismatch(f.clone(), tx.clone(), a.clone()));
             }
 
-            RetTypeOnly(tb.subst_shift(&x.into(), a))
+            let ret = tb.subst_shift(&x.into(), a);
+            ret.normalize_nf();
+            RetTypeOnly(ret)
         }
         Annot(x, t) => {
             if &x.get_type()? != t {
-- 
cgit v1.2.3