Pass TypedImproved directly to type_last_layer

1 files changed, 55 insertions, 40 deletions

diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 37c95c5..6fb7cac 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -176,6 +176,18 @@ impl TypedImproved {
             TypedImproved::Expr(e) => Ok(e),
         }
     }
+    fn normalize_to_type(self) -> Result<Type<'static>, TypeError> {
+        Ok(self.into_typed()?.normalize_to_type())
+    }
+    fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> {
+        Ok(Cow::Owned(self.clone().get_type_move()?))
+    }
+    fn get_type_move(self) -> Result<Type<'static>, TypeError> {
+        Ok(self.into_typed()?.get_type_move()?)
+    }
+    fn normalize(self) -> Result<Normalized<'static>, TypeError> {
+        Ok(self.into_typed()?.normalize())
+    }
 }
 
 #[derive(Debug, Clone)]
@@ -453,7 +465,7 @@ fn mktype(
     ctx: &TypecheckContext,
     e: SubExpr<X, Normalized<'static>>,
 ) -> Result<Type<'static>, TypeError> {
-    Ok(type_with(ctx, e)?.into_typed()?.normalize_to_type())
+    Ok(type_with(ctx, e)?.normalize_to_type()?)
 }
 
 fn into_simple_type<'a>(e: SubExpr<X, X>) -> Type<'a> {
@@ -549,7 +561,7 @@ fn type_with(
             ctx,
             // Typecheck recursively all subexpressions
             e.as_ref().traverse_ref_simple(|e| {
-                Ok(type_with(ctx, e.clone())?.into_typed()?)
+                Ok(type_with(ctx, e.clone())?)
             })?,
             e.clone(),
         ),
@@ -574,7 +586,7 @@ fn type_with(
 /// layer.
 fn type_last_layer(
     ctx: &TypecheckContext,
-    e: ExprF<Typed<'static>, Label, X, Normalized<'static>>,
+    e: ExprF<TypedImproved, Label, X, Normalized<'static>>,
     original_e: SubExpr<X, Normalized<'static>>,
 ) -> Result<Ret, TypeError> {
     use dhall_core::BinOp::*;
@@ -609,12 +621,12 @@ fn type_last_layer(
             Ok(RetExpr(Let(
                 x.clone(),
                 None,
-                a.normalize().embed(),
+                a.normalize()?.embed(),
                 tb.embed_absurd(),
             )))
         }
         Annot(x, t) => {
-            let t = t.normalize_to_type();
+            let t = t.normalize_to_type()?;
             ensure_equal!(
                 &t,
                 x.get_type()?,
@@ -648,7 +660,7 @@ fn type_last_layer(
             Ok(RetType(y.get_type_move()?))
         }
         EmptyListLit(t) => {
-            let t = t.normalize_to_type();
+            let t = t.normalize_to_type()?;
             ensure_simple_type!(
                 t,
                 mkerr(InvalidListType(t.into_normalized()?)),
@@ -679,15 +691,15 @@ fn type_last_layer(
             Ok(RetExpr(dhall::expr!(List t)))
         }
         OldOptionalLit(None, t) => {
-            let t = t.normalize().embed();
+            let t = t.normalize()?.embed();
             let e = dhall::subexpr!(None t);
             Ok(RetType(
                 type_with(ctx, e)?.into_typed()?.get_type()?.into_owned(),
             ))
         }
         OldOptionalLit(Some(x), t) => {
-            let t = t.normalize().embed();
-            let x = x.normalize().embed();
+            let t = t.normalize()?.embed();
+            let x = x.normalize()?.embed();
             let e = dhall::subexpr!(Some x : Optional t);
             Ok(RetType(
                 type_with(ctx, e)?.into_typed()?.get_type()?.into_owned(),
@@ -759,7 +771,10 @@ fn type_last_layer(
             let mut kts: std::collections::BTreeMap<_, _> = kvs
                 .into_iter()
                 .map(|(x, v)| {
-                    let t = v.map(|x| x.normalize().embed());
+                    let t = match v {
+                        Some(x) => Some(x.normalize()?.embed()),
+                        None => None,
+                    };
                     Ok((x, t))
                 })
                 .collect::<Result<_, _>>()?;
@@ -773,7 +788,7 @@ fn type_last_layer(
                 None => Err(mkerr(MissingRecordField(x, r))),
             },
             _ => {
-                let r = r.normalize_to_type();
+                let r = r.normalize_to_type()?;
                 match r.as_normalized()?.as_expr().as_ref() {
                     UnionType(kts) => match kts.get(&x) {
                         // Constructor has type T -> < x: T, ... >
@@ -860,21 +875,21 @@ pub(crate) enum TypeMessage<'a> {
     UnboundVariable(V<Label>),
     InvalidInputType(Normalized<'a>),
     InvalidOutputType(Normalized<'a>),
-    NotAFunction(Typed<'a>),
-    TypeMismatch(Typed<'a>, Normalized<'a>, Typed<'a>),
-    AnnotMismatch(Typed<'a>, Normalized<'a>),
+    NotAFunction(TypedImproved),
+    TypeMismatch(TypedImproved, Normalized<'a>, TypedImproved),
+    AnnotMismatch(TypedImproved, Normalized<'a>),
     Untyped,
-    InvalidListElement(usize, Normalized<'a>, Typed<'a>),
+    InvalidListElement(usize, Normalized<'a>, TypedImproved),
     InvalidListType(Normalized<'a>),
     InvalidOptionalType(Normalized<'a>),
-    InvalidPredicate(Typed<'a>),
-    IfBranchMismatch(Typed<'a>, Typed<'a>),
-    IfBranchMustBeTerm(bool, Typed<'a>),
-    InvalidFieldType(Label, Typed<'a>),
+    InvalidPredicate(TypedImproved),
+    IfBranchMismatch(TypedImproved, TypedImproved),
+    IfBranchMustBeTerm(bool, TypedImproved),
+    InvalidFieldType(Label, TypedImproved),
     NotARecord(Label, Normalized<'a>),
-    MissingRecordField(Label, Typed<'a>),
+    MissingRecordField(Label, TypedImproved),
     MissingUnionField(Label, Normalized<'a>),
-    BinOpTypeMismatch(BinOp, Typed<'a>),
+    BinOpTypeMismatch(BinOp, TypedImproved),
     NoDependentTypes(Normalized<'a>, Normalized<'a>),
     Unimplemented,
 }
@@ -926,25 +941,25 @@ impl fmt::Display for TypeMessage<'static> {
             // UnboundVariable(_) => {
             //     f.write_str(include_str!("errors/UnboundVariable.txt"))
             // }
-            TypeMismatch(e0, e1, e2) => {
-                let template = include_str!("errors/TypeMismatch.txt");
-                let s = template
-                    .replace("$txt0", &format!("{}", e0.as_expr()))
-                    .replace("$txt1", &format!("{}", e1.as_expr()))
-                    .replace("$txt2", &format!("{}", e2.as_expr()))
-                    .replace(
-                        "$txt3",
-                        &format!(
-                            "{}",
-                            e2.get_type()
-                                .unwrap()
-                                .as_normalized()
-                                .unwrap()
-                                .as_expr()
-                        ),
-                    );
-                f.write_str(&s)
-            }
+            // TypeMismatch(e0, e1, e2) => {
+            //     let template = include_str!("errors/TypeMismatch.txt");
+            //     let s = template
+            //         .replace("$txt0", &format!("{}", e0.as_expr()))
+            //         .replace("$txt1", &format!("{}", e1.as_expr()))
+            //         .replace("$txt2", &format!("{}", e2.as_expr()))
+            //         .replace(
+            //             "$txt3",
+            //             &format!(
+            //                 "{}",
+            //                 e2.get_type()
+            //                     .unwrap()
+            //                     .as_normalized()
+            //                     .unwrap()
+            //                     .as_expr()
+            //             ),
+            //         );
+            //     f.write_str(&s)
+            // }
             _ => f.write_str("Unhandled error message"),
         }
     }