Simplify conversions to/from TyExpr

8 files changed, 108 insertions, 108 deletions

diff --git a/dhall/src/semantics/hir.rs b/dhall/src/semantics/hir.rs
index 288031c..f91aa73 100644
--- a/dhall/src/semantics/hir.rs
+++ b/dhall/src/semantics/hir.rs
@@ -1,5 +1,6 @@
 #![allow(dead_code)]
-use crate::semantics::{NameEnv, NzEnv, TyEnv, Value};
+use crate::error::TypeError;
+use crate::semantics::{type_with, NameEnv, NzEnv, TyEnv, TyExpr, Value};
 use crate::syntax::{Expr, ExprKind, Span, V};
 use crate::{NormalizedExpr, ToExprOptions};
 
@@ -69,6 +70,11 @@ impl Hir {
         hir_to_expr(self, opts, &mut env)
     }
 
+    /// Typecheck the Hir.
+    pub fn typecheck(&self, env: &TyEnv) -> Result<TyExpr, TypeError> {
+        type_with(env, self)
+    }
+
     /// Eval the Hir. It will actually get evaluated only as needed on demand.
     pub fn eval(&self, env: &NzEnv) -> Value {
         Value::new_thunk(env.clone(), self.clone())
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index 2ae6852..0603fb5 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -1,12 +1,10 @@
 use std::collections::HashMap;
 use std::rc::Rc;
 
-use crate::error::TypeError;
 use crate::semantics::nze::lazy;
 use crate::semantics::{
-    apply_any, normalize_hir_whnf, normalize_one_layer, squash_textlit,
-    type_with, Binder, BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv,
-    TyExpr, VarEnv,
+    apply_any, normalize_hir_whnf, normalize_one_layer, squash_textlit, Binder,
+    BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, VarEnv,
 };
 use crate::syntax::{
     BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Label, LitKind,
@@ -146,8 +144,7 @@ impl Value {
         if opts.normalize {
             self.normalize();
         }
-
-        self.to_tyexpr_noenv().to_expr(opts)
+        self.to_hir_noenv().to_expr(opts)
     }
     pub(crate) fn to_expr_tyenv(&self, tyenv: &TyEnv) -> NormalizedExpr {
         self.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv)
@@ -161,10 +158,6 @@ impl Value {
         Value::from_kind(apply_any(self.clone(), v))
     }
 
-    pub(crate) fn get_type(&self, tyenv: &TyEnv) -> Result<Value, TypeError> {
-        self.to_tyexpr_tyenv(tyenv).get_type()
-    }
-
     pub fn to_hir(&self, venv: VarEnv) -> Hir {
         let map_uniontype = |kts: &HashMap<Label, Option<Value>>| {
             ExprKind::UnionType(
@@ -270,13 +263,6 @@ impl Value {
     pub fn to_hir_noenv(&self) -> Hir {
         self.to_hir(VarEnv::new())
     }
-    pub fn to_tyexpr_tyenv(&self, tyenv: &TyEnv) -> TyExpr {
-        let hir = self.to_hir(tyenv.as_varenv());
-        type_with(tyenv, &hir).unwrap()
-    }
-    pub fn to_tyexpr_noenv(&self) -> TyExpr {
-        self.to_tyexpr_tyenv(&TyEnv::new())
-    }
 }
 
 impl ValueInternal {
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index b49ea3e..dc14cd2 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,6 +1,6 @@
 use crate::error::{TypeError, TypeMessage};
-use crate::semantics::{Hir, HirKind, NzEnv, Value,TyEnv};
-use crate::syntax::Span;
+use crate::semantics::{Hir, HirKind, NzEnv, TyEnv, Value};
+use crate::syntax::{Const, Span};
 use crate::{NormalizedExpr, ToExprOptions};
 
 pub(crate) type Type = Value;
@@ -33,7 +33,12 @@ impl TyExpr {
         }
     }
     pub fn get_type_tyexpr(&self, env: &TyEnv) -> Result<TyExpr, TypeError> {
-        Ok(self.get_type()?.to_tyexpr_tyenv(env))
+        Ok(self.get_type()?.to_hir(env.as_varenv()).typecheck(env)?)
+    }
+    /// Get the kind (the type of the type) of this value
+    // TODO: avoid recomputing so much
+    pub fn get_kind(&self, env: &TyEnv) -> Result<Option<Const>, TypeError> {
+        Ok(self.get_type_tyexpr(env)?.get_type()?.as_const())
     }
 
     pub fn to_hir(&self) -> Hir {
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index c854552..794edcf 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -12,28 +12,6 @@ use crate::syntax::{
     BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, LitKind, Span,
 };
 
-fn type_of_recordtype<'a>(
-    span: Span,
-    tys: impl Iterator<Item = Cow<'a, TyExpr>>,
-) -> Result<Type, TypeError> {
-    let span_err = |msg: &str| {
-        mkerr(
-            ErrorBuilder::new(msg.to_string())
-                .span_err(span.clone(), msg.to_string())
-                .format(),
-        )
-    };
-    // An empty record type has type Type
-    let mut k = Const::Type;
-    for t in tys {
-        match t.get_type()?.as_const() {
-            Some(c) => k = max(k, c),
-            None => return span_err("InvalidFieldType"),
-        }
-    }
-    Ok(Value::from_const(k))
-}
-
 fn function_check(a: Const, b: Const) -> Const {
     if b == Const::Type {
         Const::Type
@@ -42,8 +20,19 @@ fn function_check(a: Const, b: Const) -> Const {
     }
 }
 
-pub fn mkerr<T, S: ToString>(x: S) -> Result<T, TypeError> {
-    Err(TypeError::new(TypeMessage::Custom(x.to_string())))
+pub fn mkerr<T, S: ToString>(msg: S) -> Result<T, TypeError> {
+    Err(TypeError::new(TypeMessage::Custom(msg.to_string())))
+}
+
+pub fn mk_span_err<T, S: ToString>(
+    span: &Span,
+    msg: S,
+) -> Result<T, TypeError> {
+    mkerr(
+        ErrorBuilder::new(msg.to_string())
+            .span_err(span.clone(), msg.to_string())
+            .format(),
+    )
 }
 
 /// When all sub-expressions have been typed, check the remaining toplevel
@@ -53,13 +42,7 @@ fn type_one_layer(
     ekind: ExprKind<TyExpr>,
     span: Span,
 ) -> Result<TyExpr, TypeError> {
-    let span_err = |msg: &str| {
-        mkerr(
-            ErrorBuilder::new(msg.to_string())
-                .span_err(span.clone(), msg.to_string())
-                .format(),
-        )
-    };
+    let span_err = |msg: &str| mk_span_err(&span, msg);
 
     let ty = match &ekind {
         ExprKind::Import(..) => unreachable!(
@@ -68,10 +51,9 @@ fn type_one_layer(
         ExprKind::Var(..) | ExprKind::Const(Const::Sort) => unreachable!(), // Handled in type_with
 
         ExprKind::Lam(binder, annot, body) => {
-            let body_ty = body.get_type()?;
-            let body_ty = body_ty.to_tyexpr_tyenv(
+            let body_ty = body.get_type_tyexpr(
                 &env.insert_type(&binder.clone(), annot.eval(env)),
-            );
+            )?;
             let pi_ekind = ExprKind::Pi(binder.clone(), annot.clone(), body_ty);
             type_one_layer(env, pi_ekind, Span::Artificial)?.eval(env)
         }
@@ -157,19 +139,19 @@ fn type_one_layer(
                     return span_err("InvalidListElement");
                 }
             }
-            let t = x.get_type()?;
-            if t.get_type(env)?.as_const() != Some(Const::Type) {
+            if x.get_kind(env)? != Some(Const::Type) {
                 return span_err("InvalidListType");
             }
 
+            let t = x.get_type()?;
             Value::from_builtin(Builtin::List).app(t)
         }
         ExprKind::SomeLit(x) => {
-            let t = x.get_type()?;
-            if t.get_type(env)?.as_const() != Some(Const::Type) {
+            if x.get_kind(env)? != Some(Const::Type) {
                 return span_err("InvalidOptionalType");
             }
 
+            let t = x.get_type()?;
             Value::from_builtin(Builtin::Optional).app(t)
         }
         ExprKind::RecordLit(kvs) => {
@@ -183,18 +165,23 @@ fn type_one_layer(
                     }
                     Entry::Vacant(e) => e.insert(v.get_type()?),
                 };
+
+                // Check that the fields have a valid kind
+                match v.get_kind(env)? {
+                    Some(_) => {}
+                    None => return span_err("InvalidFieldType"),
+                }
             }
 
-            type_of_recordtype(
-                span.clone(),
-                kts.iter().map(|(_, t)| Cow::Owned(t.to_tyexpr_tyenv(env))),
-            )?;
             Value::from_kind(ValueKind::RecordType(kts))
         }
         ExprKind::RecordType(kts) => {
             use std::collections::hash_map::Entry;
             let mut seen_fields = HashMap::new();
-            for (x, _) in kts {
+            // An empty record type has type Type
+            let mut k = Const::Type;
+
+            for (x, t) in kts {
                 // Check for duplicated entries
                 match seen_fields.entry(x.clone()) {
                     Entry::Occupied(_) => {
@@ -202,12 +189,15 @@ fn type_one_layer(
                     }
                     Entry::Vacant(e) => e.insert(()),
                 };
+
+                // Check the type is a Const and compute final type
+                match t.get_type()?.as_const() {
+                    Some(c) => k = max(k, c),
+                    None => return span_err("InvalidFieldType"),
+                }
             }
 
-            type_of_recordtype(
-                span.clone(),
-                kts.iter().map(|(_, t)| Cow::Borrowed(t)),
-            )?
+            Value::from_const(k)
         }
         ExprKind::UnionType(kts) => {
             use std::collections::hash_map::Entry;
@@ -337,9 +327,7 @@ fn type_one_layer(
             if *x.get_type()?.kind() != ValueKind::from_builtin(Builtin::Bool) {
                 return span_err("InvalidPredicate");
             }
-            let y_ty = y.get_type()?;
-            let y_ty = y_ty.to_tyexpr_tyenv(env);
-            if y_ty.get_type()?.as_const() != Some(Const::Type) {
+            if y.get_kind(env)? != Some(Const::Type) {
                 return span_err("IfBranchMustBeTerm");
             }
             if y.get_type()? != z.get_type()? {
@@ -369,45 +357,44 @@ fn type_one_layer(
                 Ok(r_t.clone())
             })?;
 
-            // Construct the final record type
-            type_of_recordtype(
-                span.clone(),
-                kts.iter().map(|(_, t)| Cow::Owned(t.to_tyexpr_tyenv(env))),
-            )?;
             Value::from_kind(ValueKind::RecordType(kts))
         }
         ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => {
             let ekind = ExprKind::BinOp(
                 BinOp::RecursiveRecordTypeMerge,
-                x.get_type()?.to_tyexpr_tyenv(env),
-                y.get_type()?.to_tyexpr_tyenv(env),
+                x.get_type_tyexpr(env)?,
+                y.get_type_tyexpr(env)?,
             );
-            type_one_layer(env, ekind, Span::Artificial)?.eval(env)
+            type_one_layer(env, ekind, span.clone())?.eval(env)
         }
         ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => {
-            let x_val = x.eval(env);
-            let y_val = y.eval(env);
-            let kts_x = match x_val.kind() {
-                ValueKind::RecordType(kts) => kts,
-                _ => return span_err("RecordTypeMergeRequiresRecordType"),
-            };
-            let kts_y = match y_val.kind() {
-                ValueKind::RecordType(kts) => kts,
-                _ => return span_err("RecordTypeMergeRequiresRecordType"),
-            };
-            for (k, tx) in kts_x {
-                if let Some(ty) = kts_y.get(k) {
-                    type_one_layer(
-                        env,
-                        ExprKind::BinOp(
-                            BinOp::RecursiveRecordTypeMerge,
-                            tx.to_tyexpr_tyenv(env),
-                            ty.to_tyexpr_tyenv(env),
-                        ),
-                        Span::Artificial,
-                    )?;
+            fn check_rectymerge(
+                span: &Span,
+                env: &TyEnv,
+                x: Type,
+                y: Type,
+            ) -> Result<(), TypeError> {
+                let kts_x = match x.kind() {
+                    ValueKind::RecordType(kts) => kts,
+                    _ => return mk_span_err(span, "RecordTypeMergeRequiresRecordType"),
+                };
+                let kts_y = match y.kind() {
+                    ValueKind::RecordType(kts) => kts,
+                    _ => return mk_span_err(span, "RecordTypeMergeRequiresRecordType"),
+                };
+                for (k, tx) in kts_x {
+                    if let Some(ty) = kts_y.get(k) {
+                        check_rectymerge(
+                            span,
+                            env,
+                            tx.clone(),
+                            ty.clone(),
+                        )?;
+                    }
                 }
+                Ok(())
             }
+            check_rectymerge(&span, env, x.eval(env), y.eval(env))?;
 
             // A RecordType's type is always a const
             let xk = x.get_type()?.as_const().unwrap();
@@ -434,9 +421,7 @@ fn type_one_layer(
             if l.get_type()? != r.get_type()? {
                 return span_err("EquivalenceTypeMismatch");
             }
-            if l.get_type()?.to_tyexpr_tyenv(env).get_type()?.as_const()
-                != Some(Const::Type)
-            {
+            if l.get_kind(env)? != Some(Const::Type) {
                 return span_err("EquivalenceArgumentsMustBeTerms");
             }
 
@@ -605,6 +590,9 @@ fn type_one_layer(
             }
         }
         ExprKind::ToMap(record, annot) => {
+            if record.get_kind(env)? != Some(Const::Type) {
+                return span_err("`toMap` only accepts records of type `Type`");
+            }
             let record_t = record.get_type()?;
             let kts = match record_t.kind() {
                 ValueKind::RecordType(kts) => kts,
@@ -652,11 +640,6 @@ fn type_one_layer(
                 annot_val
             } else {
                 let entry_type = kts.iter().next().unwrap().1.clone();
-                if entry_type.get_type(env)?.as_const() != Some(Const::Type) {
-                    return span_err(
-                        "`toMap` only accepts records of type `Type`",
-                    );
-                }
                 for (_, t) in kts.iter() {
                     if *t != entry_type {
                         return span_err(
diff --git a/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeLhsNotRecord.txt b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeLhsNotRecord.txt
index f74e839..02cf64f 100644
--- a/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeLhsNotRecord.txt
+++ b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeLhsNotRecord.txt
@@ -1 +1,6 @@
 Type error: error: RecordTypeMergeRequiresRecordType
+ --> <current file>:1:0
+  |
+1 | True ∧ {=}
+  | ^^^^^^^^^^ RecordTypeMergeRequiresRecordType
+  |
diff --git a/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeOverlapping.txt b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeOverlapping.txt
index f74e839..202a3e5 100644
--- a/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeOverlapping.txt
+++ b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeOverlapping.txt
@@ -1 +1,6 @@
 Type error: error: RecordTypeMergeRequiresRecordType
+ --> <current file>:1:0
+  |
+1 | { x = True } ∧ { x = False }
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ RecordTypeMergeRequiresRecordType
+  |
diff --git a/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeRhsNotRecord.txt b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeRhsNotRecord.txt
index f74e839..a0b4676 100644
--- a/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeRhsNotRecord.txt
+++ b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeRhsNotRecord.txt
@@ -1 +1,6 @@
 Type error: error: RecordTypeMergeRequiresRecordType
+ --> <current file>:1:0
+  |
+1 | {=} ∧ True
+  | ^^^^^^^^^^ RecordTypeMergeRequiresRecordType
+  |
diff --git a/dhall/tests/type-inference/failure/unit/RecursiveRecordTypeMergeOverlapping.txt b/dhall/tests/type-inference/failure/unit/RecursiveRecordTypeMergeOverlapping.txt
index f74e839..769712b 100644
--- a/dhall/tests/type-inference/failure/unit/RecursiveRecordTypeMergeOverlapping.txt
+++ b/dhall/tests/type-inference/failure/unit/RecursiveRecordTypeMergeOverlapping.txt
@@ -1 +1,6 @@
 Type error: error: RecordTypeMergeRequiresRecordType
+ --> <current file>:1:0
+  |
+1 | { x : Bool } ⩓ { x : Natural }
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ RecordTypeMergeRequiresRecordType
+  |