From db1375eccd1e6943b504cd54ed17eb8f4d19c25f Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 6 Feb 2020 17:35:54 +0000
Subject: Remove most reliance on types stored in Value

---
 dhall/src/semantics/tck/env.rs       |  8 +++---
 dhall/src/semantics/tck/typecheck.rs | 56 ++++++++++++++++++++----------------
 2 files changed, 35 insertions(+), 29 deletions(-)

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

diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index 1fc711c..b3e7895 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -104,16 +104,16 @@ impl TyEnv {
         &self.names
     }
 
-    pub fn insert_type(&self, x: &Label, t: Type) -> Self {
+    pub fn insert_type(&self, x: &Label, ty: Type) -> Self {
         TyEnv {
             names: self.names.insert(x),
-            items: self.items.insert_type(t),
+            items: self.items.insert_type(ty),
         }
     }
-    pub fn insert_value(&self, x: &Label, e: Value) -> Self {
+    pub fn insert_value(&self, x: &Label, e: Value, ty: Type) -> Self {
         TyEnv {
             names: self.names.insert(x),
-            items: self.items.insert_value(e),
+            items: self.items.insert_value(e, ty),
         }
     }
     pub fn lookup(&self, var: &V) -> Option<(AlphaVar, Type)> {
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index dd9a8fa..ceb83de 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -72,7 +72,9 @@ fn type_one_layer(
 
         ExprKind::Lam(binder, annot, body) => {
             let body_ty = body.get_type()?;
-            let body_ty = body_ty.to_tyexpr(env.as_varenv().insert());
+            let body_ty = body_ty.to_tyexpr_tyenv(
+                &env.insert_type(&binder.clone(), annot.eval(env.as_nzenv())),
+            );
             let pi_ekind = ExprKind::Pi(binder.clone(), annot.clone(), body_ty);
             type_one_layer(env, pi_ekind, Span::Artificial)?
                 .eval(env.as_nzenv())
@@ -154,7 +156,7 @@ fn type_one_layer(
                 }
             }
             let t = x.get_type()?;
-            if t.get_type()?.as_const() != Some(Const::Type) {
+            if t.get_type(env)?.as_const() != Some(Const::Type) {
                 return span_err("InvalidListType");
             }
 
@@ -162,7 +164,7 @@ fn type_one_layer(
         }
         ExprKind::SomeLit(x) => {
             let t = x.get_type()?;
-            if t.get_type()?.as_const() != Some(Const::Type) {
+            if t.get_type(env)?.as_const() != Some(Const::Type) {
                 return span_err("InvalidOptionalType");
             }
 
@@ -183,8 +185,7 @@ fn type_one_layer(
 
             let ty = type_of_recordtype(
                 span.clone(),
-                kts.iter()
-                    .map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_varenv()))),
+                kts.iter().map(|(_, t)| Cow::Owned(t.to_tyexpr_tyenv(env))),
             )?;
             Value::from_kind_and_type(ValueKind::RecordType(kts), ty)
         }
@@ -278,13 +279,13 @@ fn type_one_layer(
                 return span_err(&format!(
                     "annot mismatch: ({} : {}) : {}",
                     x.to_expr_tyenv(env),
-                    x_ty.to_tyexpr(env.as_varenv()).to_expr_tyenv(env),
-                    t.to_tyexpr(env.as_varenv()).to_expr_tyenv(env)
+                    x_ty.to_tyexpr_tyenv(env).to_expr_tyenv(env),
+                    t.to_tyexpr_tyenv(env).to_expr_tyenv(env)
                 ));
                 // return span_err(format!(
                 //     "annot mismatch: {} != {}",
-                //     x_ty.to_tyexpr(env.as_varenv()).to_expr_tyenv(env),
-                //     t.to_tyexpr(env.as_varenv()).to_expr_tyenv(env)
+                //     x_ty.to_tyexpr_tyenv(env).to_expr_tyenv(env),
+                //     t.to_tyexpr_tyenv(env).to_expr_tyenv(env)
                 // ));
                 // return span_err(format!("annot mismatch: {:#?} : {:#?}", x, t,));
             }
@@ -352,10 +353,9 @@ fn type_one_layer(
             if *x.get_type()?.kind() != ValueKind::from_builtin(Builtin::Bool) {
                 return span_err("InvalidPredicate");
             }
-            if y.get_type()?.get_type()?.as_const() != Some(Const::Type) {
-                return span_err("IfBranchMustBeTerm");
-            }
-            if z.get_type()?.get_type()?.as_const() != Some(Const::Type) {
+            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) {
                 return span_err("IfBranchMustBeTerm");
             }
             if y.get_type()? != z.get_type()? {
@@ -388,16 +388,15 @@ fn type_one_layer(
             // Construct the final record type
             let ty = type_of_recordtype(
                 span.clone(),
-                kts.iter()
-                    .map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_varenv()))),
+                kts.iter().map(|(_, t)| Cow::Owned(t.to_tyexpr_tyenv(env))),
             )?;
             Value::from_kind_and_type(ValueKind::RecordType(kts), ty)
         }
         ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => {
             let ekind = ExprKind::BinOp(
                 BinOp::RecursiveRecordTypeMerge,
-                x.get_type()?.to_tyexpr(env.as_varenv()),
-                y.get_type()?.to_tyexpr(env.as_varenv()),
+                x.get_type()?.to_tyexpr_tyenv(env),
+                y.get_type()?.to_tyexpr_tyenv(env),
             );
             type_one_layer(env, ekind, Span::Artificial)?.eval(env.as_nzenv())
         }
@@ -418,8 +417,8 @@ fn type_one_layer(
                         env,
                         ExprKind::BinOp(
                             BinOp::RecursiveRecordTypeMerge,
-                            tx.to_tyexpr(env.as_varenv()),
-                            ty.to_tyexpr(env.as_varenv()),
+                            tx.to_tyexpr_tyenv(env),
+                            ty.to_tyexpr_tyenv(env),
                         ),
                         Span::Artificial,
                     )?;
@@ -451,7 +450,9 @@ fn type_one_layer(
             if l.get_type()? != r.get_type()? {
                 return span_err("EquivalenceTypeMismatch");
             }
-            if l.get_type()?.get_type()?.as_const() != Some(Const::Type) {
+            if l.get_type()?.to_tyexpr_tyenv(env).get_type()?.as_const()
+                != Some(Const::Type)
+            {
                 return span_err("EquivalenceArgumentsMustBeTerms");
             }
 
@@ -668,7 +669,7 @@ fn type_one_layer(
                 annot_val
             } else {
                 let entry_type = kts.iter().next().unwrap().1.clone();
-                if entry_type.get_type()?.as_const() != Some(Const::Type) {
+                if entry_type.get_type(env)?.as_const() != Some(Const::Type) {
                     return span_err(
                         "`toMap` only accepts records of type `Type`",
                     );
@@ -724,7 +725,7 @@ fn type_one_layer(
 
             Value::from_kind_and_type(
                 ValueKind::RecordType(new_kts),
-                record_type.get_type()?,
+                record_type.get_type(env)?,
             )
         }
         ExprKind::ProjectionByExpr(record, selection) => {
@@ -804,7 +805,12 @@ pub(crate) fn type_with(
             (TyExprKind::Expr(ExprKind::Const(Const::Sort)), None)
         }
         ExprKind::Embed(p) => {
-            return Ok(p.clone().into_value().to_tyexpr_noenv())
+            let val = p.clone().into_value();
+            (
+                val.to_tyexpr_noenv().kind().clone(),
+                Some(val.get_type(&TyEnv::new())?),
+            )
+            // return Ok(p.clone().into_value().to_tyexpr_noenv())
         }
         ekind => {
             let ekind = match ekind {
@@ -829,9 +835,9 @@ pub(crate) fn type_with(
                         val.clone()
                     };
                     let val = type_with(env, &val)?;
-                    val.get_type()?; // Ensure val is not Sort
+                    let val_ty = val.get_type()?;
                     let val_nf = val.eval(&env.as_nzenv());
-                    let body_env = env.insert_value(&binder, val_nf);
+                    let body_env = env.insert_value(&binder, val_nf, val_ty);
                     let body = type_with(&body_env, body)?;
                     ExprKind::Let(binder.clone(), None, val, body)
                 }
-- 
cgit v1.2.3


From 5870a46d5ab5810901198f03ed461d5c3bb5aa8a Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 6 Feb 2020 17:58:48 +0000
Subject: Remove move type propagation through Value

---
 dhall/src/semantics/tck/typecheck.rs | 42 +++++++++++-------------------------
 1 file changed, 12 insertions(+), 30 deletions(-)

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

diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index ceb83de..810e483 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -183,11 +183,11 @@ fn type_one_layer(
                 };
             }
 
-            let ty = type_of_recordtype(
+            type_of_recordtype(
                 span.clone(),
                 kts.iter().map(|(_, t)| Cow::Owned(t.to_tyexpr_tyenv(env))),
             )?;
-            Value::from_kind_and_type(ValueKind::RecordType(kts), ty)
+            Value::from_kind(ValueKind::RecordType(kts))
         }
         ExprKind::RecordType(kts) => {
             use std::collections::hash_map::Entry;
@@ -247,22 +247,11 @@ fn type_one_layer(
                         ValueKind::UnionType(kts) => match kts.get(x) {
                             // Constructor has type T -> < x: T, ... >
                             Some(Some(ty)) => {
-                                // Can't fail because uniontypes must have type Const(_).
-                                let kt = scrut.get_type()?.as_const().unwrap();
-                                // The type of the field must be Const smaller than `kt`, thus the
-                                // function type has type `kt`.
-                                let pi_ty = Value::from_const(kt);
-
-                                Value::from_kind_and_type(
-                                    ValueKind::PiClosure {
-                                        binder: Binder::new(x.clone()),
-                                        annot: ty.clone(),
-                                        closure: Closure::new_constant(
-                                            scrut_nf,
-                                        ),
-                                    },
-                                    pi_ty,
-                                )
+                                Value::from_kind(ValueKind::PiClosure {
+                                    binder: Binder::new(x.clone()),
+                                    annot: ty.clone(),
+                                    closure: Closure::new_constant(scrut_nf),
+                                })
                             }
                             Some(None) => scrut_nf,
                             None => return span_err("MissingUnionField"),
@@ -386,11 +375,11 @@ fn type_one_layer(
             })?;
 
             // Construct the final record type
-            let ty = type_of_recordtype(
+            type_of_recordtype(
                 span.clone(),
                 kts.iter().map(|(_, t)| Cow::Owned(t.to_tyexpr_tyenv(env))),
             )?;
-            Value::from_kind_and_type(ValueKind::RecordType(kts), ty)
+            Value::from_kind(ValueKind::RecordType(kts))
         }
         ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => {
             let ekind = ExprKind::BinOp(
@@ -685,12 +674,8 @@ fn type_one_layer(
                 let mut kts = HashMap::new();
                 kts.insert("mapKey".into(), Value::from_builtin(Builtin::Text));
                 kts.insert("mapValue".into(), entry_type);
-                let output_type = Value::from_builtin(Builtin::List).app(
-                    Value::from_kind_and_type(
-                        ValueKind::RecordType(kts),
-                        Value::from_const(Const::Type),
-                    ),
-                );
+                let output_type = Value::from_builtin(Builtin::List)
+                    .app(Value::from_kind(ValueKind::RecordType(kts)));
                 if let Some(annot) = annot {
                     let annot_val = annot.eval(env.as_nzenv());
                     if output_type != annot_val {
@@ -723,10 +708,7 @@ fn type_one_layer(
                 };
             }
 
-            Value::from_kind_and_type(
-                ValueKind::RecordType(new_kts),
-                record_type.get_type(env)?,
-            )
+            Value::from_kind(ValueKind::RecordType(new_kts))
         }
         ExprKind::ProjectionByExpr(record, selection) => {
             let record_type = record.get_type()?;
-- 
cgit v1.2.3


From 27031b3739ff9f2043e64130a4c5699d0f9233e8 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 9 Feb 2020 11:23:59 +0000
Subject: Add Hir as untyped alternative to TyExpr

---
 dhall/src/semantics/tck/tyexpr.rs | 70 +++++++--------------------------------
 1 file changed, 12 insertions(+), 58 deletions(-)

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

diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index 1886646..fa578c0 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,17 +1,13 @@
 use crate::error::{TypeError, TypeMessage};
-use crate::semantics::{rc, NameEnv, NzEnv, TyEnv, Value};
+use crate::semantics::{
+    rc, AlphaVar, Hir, HirKind, NameEnv, NzEnv, TyEnv, Value,
+};
 use crate::syntax::{ExprKind, Span, V};
 use crate::Normalized;
 use crate::{NormalizedExpr, ToExprOptions};
 
 pub(crate) type Type = Value;
 
-/// Stores an alpha-normalized variable.
-#[derive(Debug, Clone, Copy)]
-pub struct AlphaVar {
-    idx: usize,
-}
-
 #[derive(Debug, Clone)]
 pub(crate) enum TyExprKind {
     Var(AlphaVar),
@@ -27,15 +23,6 @@ pub(crate) struct TyExpr {
     span: Span,
 }
 
-impl AlphaVar {
-    pub(crate) fn new(idx: usize) -> Self {
-        AlphaVar { idx }
-    }
-    pub(crate) fn idx(&self) -> usize {
-        self.idx
-    }
-}
-
 impl TyExpr {
     pub fn new(kind: TyExprKind, ty: Option<Type>, span: Span) -> Self {
         TyExpr {
@@ -58,17 +45,19 @@ impl TyExpr {
         }
     }
 
+    pub fn to_hir(&self) -> Hir {
+        let kind = match self.kind() {
+            TyExprKind::Var(v) => HirKind::Var(v.clone()),
+            TyExprKind::Expr(e) => HirKind::Expr(e.map_ref(|tye| tye.to_hir())),
+        };
+        Hir::new(kind, self.span())
+    }
     /// Converts a value back to the corresponding AST expression.
     pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
-        tyexpr_to_expr(self, opts, &mut NameEnv::new())
+        self.to_hir().to_expr(opts)
     }
     pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
-        let opts = ToExprOptions {
-            normalize: true,
-            alpha: false,
-        };
-        let mut env = env.as_nameenv().clone();
-        tyexpr_to_expr(self, opts, &mut env)
+        self.to_hir().to_expr_tyenv(env)
     }
 
     /// Eval the TyExpr. It will actually get evaluated only as needed on demand.
@@ -88,41 +77,6 @@ impl TyExpr {
     }
 }
 
-fn tyexpr_to_expr<'a>(
-    tyexpr: &'a TyExpr,
-    opts: ToExprOptions,
-    env: &mut NameEnv,
-) -> NormalizedExpr {
-    rc(match tyexpr.kind() {
-        TyExprKind::Var(v) if opts.alpha => {
-            ExprKind::Var(V("_".into(), v.idx()))
-        }
-        TyExprKind::Var(v) => ExprKind::Var(env.label_var(v)),
-        TyExprKind::Expr(e) => {
-            let e = e.map_ref_maybe_binder(|l, tye| {
-                if let Some(l) = l {
-                    env.insert_mut(l);
-                }
-                let e = tyexpr_to_expr(tye, opts, env);
-                if let Some(_) = l {
-                    env.remove_mut();
-                }
-                e
-            });
-
-            match e {
-                ExprKind::Lam(_, t, e) if opts.alpha => {
-                    ExprKind::Lam("_".into(), t, e)
-                }
-                ExprKind::Pi(_, t, e) if opts.alpha => {
-                    ExprKind::Pi("_".into(), t, e)
-                }
-                e => e,
-            }
-        }
-    })
-}
-
 impl std::fmt::Debug for TyExpr {
     fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         let mut x = fmt.debug_struct("TyExpr");
-- 
cgit v1.2.3


From 6c90d356c9a4a5bbeb88f25ad0ab499ba1503eae Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 9 Feb 2020 11:53:55 +0000
Subject: Remove most TyExpr from normalization

---
 dhall/src/semantics/tck/env.rs       |  6 +++---
 dhall/src/semantics/tck/tyexpr.rs    | 11 +++--------
 dhall/src/semantics/tck/typecheck.rs | 13 +++----------
 3 files changed, 9 insertions(+), 21 deletions(-)

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

diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index b3e7895..af955f4 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -21,9 +21,9 @@ pub(crate) struct TyEnv {
 }
 
 impl VarEnv {
-    pub fn new() -> Self {
-        VarEnv { size: 0 }
-    }
+    // pub fn new() -> Self {
+    //     VarEnv { size: 0 }
+    // }
     pub fn size(&self) -> usize {
         self.size
     }
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index fa578c0..29099c5 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,8 +1,6 @@
 use crate::error::{TypeError, TypeMessage};
-use crate::semantics::{
-    rc, AlphaVar, Hir, HirKind, NameEnv, NzEnv, TyEnv, Value,
-};
-use crate::syntax::{ExprKind, Span, V};
+use crate::semantics::{AlphaVar, Hir, HirKind, NzEnv, Value};
+use crate::syntax::{ExprKind, Span};
 use crate::Normalized;
 use crate::{NormalizedExpr, ToExprOptions};
 
@@ -56,13 +54,10 @@ impl TyExpr {
     pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
         self.to_hir().to_expr(opts)
     }
-    pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
-        self.to_hir().to_expr_tyenv(env)
-    }
 
     /// Eval the TyExpr. It will actually get evaluated only as needed on demand.
     pub fn eval(&self, env: &NzEnv) -> Value {
-        Value::new_thunk(env, self.clone())
+        Value::new_thunk(env, self.to_hir())
     }
     /// Eval a closed TyExpr (i.e. without free variables). It will actually get evaluated only as
     /// needed on demand.
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 810e483..5b233f8 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -266,17 +266,10 @@ fn type_one_layer(
             let x_ty = x.get_type()?;
             if x_ty != t {
                 return span_err(&format!(
-                    "annot mismatch: ({} : {}) : {}",
-                    x.to_expr_tyenv(env),
-                    x_ty.to_tyexpr_tyenv(env).to_expr_tyenv(env),
-                    t.to_tyexpr_tyenv(env).to_expr_tyenv(env)
+                    "annot mismatch: {} != {}",
+                    x_ty.to_expr_tyenv(env),
+                    t.to_expr_tyenv(env)
                 ));
-                // return span_err(format!(
-                //     "annot mismatch: {} != {}",
-                //     x_ty.to_tyexpr_tyenv(env).to_expr_tyenv(env),
-                //     t.to_tyexpr_tyenv(env).to_expr_tyenv(env)
-                // ));
-                // return span_err(format!("annot mismatch: {:#?} : {:#?}", x, t,));
             }
             x_ty
         }
-- 
cgit v1.2.3


From a709c65eb28f1b6a666f15bfc2255da7bc7105ab Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 9 Feb 2020 21:38:37 +0000
Subject: Resolve variables alongside import resolution

---
 dhall/src/semantics/tck/typecheck.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 5b233f8..eb6a58c 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -43,7 +43,7 @@ fn function_check(a: Const, b: Const) -> Const {
     }
 }
 
-fn mkerr<T, S: ToString>(x: S) -> Result<T, TypeError> {
+pub fn mkerr<T, S: ToString>(x: S) -> Result<T, TypeError> {
     Err(TypeError::new(TypeMessage::Custom(x.to_string())))
 }
 
-- 
cgit v1.2.3


From 21db63d3e614554f258526182c7ed89a2c244b65 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 9 Feb 2020 21:58:28 +0000
Subject: Take Hir for typecheck

---
 dhall/src/semantics/tck/env.rs       | 12 +++-----
 dhall/src/semantics/tck/typecheck.rs | 60 +++++++++++++++++-------------------
 2 files changed, 33 insertions(+), 39 deletions(-)

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

diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index af955f4..3b02074 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -21,9 +21,9 @@ pub(crate) struct TyEnv {
 }
 
 impl VarEnv {
-    // pub fn new() -> Self {
-    //     VarEnv { size: 0 }
-    // }
+    pub fn new() -> Self {
+        VarEnv { size: 0 }
+    }
     pub fn size(&self) -> usize {
         self.size
     }
@@ -116,9 +116,7 @@ impl TyEnv {
             items: self.items.insert_value(e, ty),
         }
     }
-    pub fn lookup(&self, var: &V) -> Option<(AlphaVar, Type)> {
-        let var = self.names.unlabel_var(var)?;
-        let ty = self.items.lookup_ty(&var);
-        Some((var, ty))
+    pub fn lookup(&self, var: &AlphaVar) -> Type {
+        self.items.lookup_ty(&var)
     }
 }
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index eb6a58c..ac113cd 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -5,11 +5,11 @@ use std::collections::HashMap;
 use crate::error::{ErrorBuilder, TypeError, TypeMessage};
 use crate::semantics::merge_maps;
 use crate::semantics::{
-    type_of_builtin, Binder, BuiltinClosure, Closure, TyEnv, TyExpr,
-    TyExprKind, Type, Value, ValueKind,
+    type_of_builtin, Binder, BuiltinClosure, Closure, Hir, HirKind, TyEnv,
+    TyExpr, TyExprKind, Type, Value, ValueKind,
 };
 use crate::syntax::{
-    BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Span,
+    BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Span,
 };
 use crate::Normalized;
 
@@ -115,8 +115,8 @@ fn type_one_layer(
         ExprKind::Const(Const::Type) => Value::from_const(Const::Kind),
         ExprKind::Const(Const::Kind) => Value::from_const(Const::Sort),
         ExprKind::Builtin(b) => {
-            let t_expr = type_of_builtin(*b);
-            let t_tyexpr = type_with(env, &t_expr)?;
+            let t_hir = type_of_builtin(*b);
+            let t_tyexpr = typecheck(&t_hir)?;
             t_tyexpr.eval(env.as_nzenv())
         }
         ExprKind::BoolLit(_) => Value::from_builtin(Builtin::Bool),
@@ -761,25 +761,16 @@ fn type_one_layer(
 }
 
 /// `type_with` typechecks an expressio in the provided environment.
-pub(crate) fn type_with(
-    env: &TyEnv,
-    expr: &Expr<Normalized>,
-) -> Result<TyExpr, TypeError> {
-    let (tyekind, ty) = match expr.as_ref() {
-        ExprKind::Var(var) => match env.lookup(&var) {
-            Some((v, ty)) => (TyExprKind::Var(v), Some(ty)),
-            None => {
-                return mkerr(
-                    ErrorBuilder::new(format!("unbound variable `{}`", var))
-                        .span_err(expr.span(), "not found in this scope")
-                        .format(),
-                )
-            }
-        },
-        ExprKind::Const(Const::Sort) => {
+pub(crate) fn type_with(env: &TyEnv, hir: &Hir) -> Result<TyExpr, TypeError> {
+    let (tyekind, ty) = match hir.kind() {
+        HirKind::Var(var) => (TyExprKind::Var(*var), Some(env.lookup(&var))),
+        HirKind::Expr(ExprKind::Var(_)) => {
+            unreachable!("Hir should contain no unresolved variables")
+        }
+        HirKind::Expr(ExprKind::Const(Const::Sort)) => {
             (TyExprKind::Expr(ExprKind::Const(Const::Sort)), None)
         }
-        ExprKind::Embed(p) => {
+        HirKind::Expr(ExprKind::Embed(p)) => {
             let val = p.clone().into_value();
             (
                 val.to_tyexpr_noenv().kind().clone(),
@@ -787,7 +778,7 @@ pub(crate) fn type_with(
             )
             // return Ok(p.clone().into_value().to_tyexpr_noenv())
         }
-        ekind => {
+        HirKind::Expr(ekind) => {
             let ekind = match ekind {
                 ExprKind::Lam(binder, annot, body) => {
                     let annot = type_with(env, annot)?;
@@ -805,7 +796,13 @@ pub(crate) fn type_with(
                 }
                 ExprKind::Let(binder, annot, val, body) => {
                     let val = if let Some(t) = annot {
-                        t.rewrap(ExprKind::Annot(val.clone(), t.clone()))
+                        Hir::new(
+                            HirKind::Expr(ExprKind::Annot(
+                                val.clone(),
+                                t.clone(),
+                            )),
+                            t.span(),
+                        )
                     } else {
                         val.clone()
                     };
@@ -818,16 +815,16 @@ pub(crate) fn type_with(
                 }
                 _ => ekind.traverse_ref(|e| type_with(env, e))?,
             };
-            return type_one_layer(env, ekind, expr.span());
+            return type_one_layer(env, ekind, hir.span());
         }
     };
 
-    Ok(TyExpr::new(tyekind, ty, expr.span()))
+    Ok(TyExpr::new(tyekind, ty, hir.span()))
 }
 
 /// Typecheck an expression and return the expression annotated with types if type-checking
 /// succeeded, or an error if type-checking failed.
-pub(crate) fn typecheck(e: &Expr<Normalized>) -> Result<TyExpr, TypeError> {
+pub(crate) fn typecheck(e: &Hir) -> Result<TyExpr, TypeError> {
     let res = type_with(&TyEnv::new(), e)?;
     // Ensure that the inferred type exists (i.e. this is not Sort)
     res.get_type()?;
@@ -835,9 +832,8 @@ pub(crate) fn typecheck(e: &Expr<Normalized>) -> Result<TyExpr, TypeError> {
 }
 
 /// Like `typecheck`, but additionally checks that the expression's type matches the provided type.
-pub(crate) fn typecheck_with(
-    expr: &Expr<Normalized>,
-    ty: Expr<Normalized>,
-) -> Result<TyExpr, TypeError> {
-    typecheck(&expr.rewrap(ExprKind::Annot(expr.clone(), ty)))
+pub(crate) fn typecheck_with(hir: &Hir, ty: Hir) -> Result<TyExpr, TypeError> {
+    let hir =
+        Hir::new(HirKind::Expr(ExprKind::Annot(hir.clone(), ty)), hir.span());
+    typecheck(&hir)
 }
-- 
cgit v1.2.3


From ad085a20bc257d03a52708d920cfc65f0e9051e6 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 9 Feb 2020 22:07:03 +0000
Subject: Remove all types from Value

---
 dhall/src/semantics/tck/tyexpr.rs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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

diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index 29099c5..05fa4b5 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -66,8 +66,8 @@ impl TyExpr {
     }
     /// Eval a closed TyExpr fully and recursively;
     pub fn rec_eval_closed_expr(&self) -> Value {
-        let mut val = self.eval_closed_expr();
-        val.normalize_mut();
+        let val = self.eval_closed_expr();
+        val.normalize();
         val
     }
 }
-- 
cgit v1.2.3


From f6732982c522dd579d378ab4820001d5ae107c43 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 9 Feb 2020 22:18:32 +0000
Subject: Automate conversion between envs

---
 dhall/src/semantics/tck/env.rs       |  6 ++++++
 dhall/src/semantics/tck/tyexpr.rs    |  4 ++--
 dhall/src/semantics/tck/typecheck.rs | 38 +++++++++++++++++-------------------
 3 files changed, 26 insertions(+), 22 deletions(-)

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

diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index 3b02074..ba7fb73 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -120,3 +120,9 @@ impl TyEnv {
         self.items.lookup_ty(&var)
     }
 }
+
+impl<'a> From<&'a TyEnv> for &'a NzEnv {
+    fn from(x: &'a TyEnv) -> Self {
+        x.as_nzenv()
+    }
+}
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index 05fa4b5..edba477 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -56,8 +56,8 @@ impl TyExpr {
     }
 
     /// Eval the TyExpr. It will actually get evaluated only as needed on demand.
-    pub fn eval(&self, env: &NzEnv) -> Value {
-        Value::new_thunk(env, self.to_hir())
+    pub fn eval<'e>(&self, env: impl Into<&'e NzEnv>) -> Value {
+        Value::new_thunk(env.into(), self.to_hir())
     }
     /// Eval a closed TyExpr (i.e. without free variables). It will actually get evaluated only as
     /// needed on demand.
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index ac113cd..7f02832 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -73,11 +73,10 @@ fn type_one_layer(
         ExprKind::Lam(binder, annot, body) => {
             let body_ty = body.get_type()?;
             let body_ty = body_ty.to_tyexpr_tyenv(
-                &env.insert_type(&binder.clone(), annot.eval(env.as_nzenv())),
+                &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.as_nzenv())
+            type_one_layer(env, pi_ekind, Span::Artificial)?.eval(env)
         }
         ExprKind::Pi(_, annot, body) => {
             let ks = match annot.get_type()?.as_const() {
@@ -117,7 +116,7 @@ fn type_one_layer(
         ExprKind::Builtin(b) => {
             let t_hir = type_of_builtin(*b);
             let t_tyexpr = typecheck(&t_hir)?;
-            t_tyexpr.eval(env.as_nzenv())
+            t_tyexpr.eval(env)
         }
         ExprKind::BoolLit(_) => Value::from_builtin(Builtin::Bool),
         ExprKind::NaturalLit(_) => Value::from_builtin(Builtin::Natural),
@@ -136,7 +135,7 @@ fn type_one_layer(
             text_type
         }
         ExprKind::EmptyListLit(t) => {
-            let t = t.eval(env.as_nzenv());
+            let t = t.eval(env);
             match &*t.kind() {
                 ValueKind::AppliedBuiltin(BuiltinClosure {
                     b: Builtin::List,
@@ -242,7 +241,7 @@ fn type_one_layer(
                 },
                 // TODO: branch here only when scrut.get_type() is a Const
                 _ => {
-                    let scrut_nf = scrut.eval(env.as_nzenv());
+                    let scrut_nf = scrut.eval(env);
                     match scrut_nf.kind() {
                         ValueKind::UnionType(kts) => match kts.get(x) {
                             // Constructor has type T -> < x: T, ... >
@@ -262,7 +261,7 @@ fn type_one_layer(
             }
         }
         ExprKind::Annot(x, t) => {
-            let t = t.eval(env.as_nzenv());
+            let t = t.eval(env);
             let x_ty = x.get_type()?;
             if x_ty != t {
                 return span_err(&format!(
@@ -274,7 +273,7 @@ fn type_one_layer(
             x_ty
         }
         ExprKind::Assert(t) => {
-            let t = t.eval(env.as_nzenv());
+            let t = t.eval(env);
             match &*t.kind() {
                 ValueKind::Equivalence(x, y) if x == y => {}
                 ValueKind::Equivalence(..) => {
@@ -315,7 +314,7 @@ fn type_one_layer(
                         );
                     }
 
-                    let arg_nf = arg.eval(env.as_nzenv());
+                    let arg_nf = arg.eval(env);
                     closure.apply(arg_nf)
                 }
                 _ => return mkerr(
@@ -380,11 +379,11 @@ fn type_one_layer(
                 x.get_type()?.to_tyexpr_tyenv(env),
                 y.get_type()?.to_tyexpr_tyenv(env),
             );
-            type_one_layer(env, ekind, Span::Artificial)?.eval(env.as_nzenv())
+            type_one_layer(env, ekind, Span::Artificial)?.eval(env)
         }
         ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => {
-            let x_val = x.eval(env.as_nzenv());
-            let y_val = y.eval(env.as_nzenv());
+            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"),
@@ -589,8 +588,7 @@ fn type_one_layer(
                 }
             }
 
-            let type_annot =
-                type_annot.as_ref().map(|t| t.eval(env.as_nzenv()));
+            let type_annot = type_annot.as_ref().map(|t| t.eval(env));
             match (inferred_type, type_annot) {
                 (Some(t1), Some(t2)) => {
                     if t1 != t2 {
@@ -621,7 +619,7 @@ fn type_one_layer(
                          annotation",
                     );
                 };
-                let annot_val = annot.eval(env.as_nzenv());
+                let annot_val = annot.eval(env);
 
                 let err_msg = "The type of `toMap x` must be of the form \
                                `List { mapKey : Text, mapValue : T }`";
@@ -670,7 +668,7 @@ fn type_one_layer(
                 let output_type = Value::from_builtin(Builtin::List)
                     .app(Value::from_kind(ValueKind::RecordType(kts)));
                 if let Some(annot) = annot {
-                    let annot_val = annot.eval(env.as_nzenv());
+                    let annot_val = annot.eval(env);
                     if output_type != annot_val {
                         return span_err("Annotation mismatch");
                     }
@@ -710,7 +708,7 @@ fn type_one_layer(
                 _ => return span_err("ProjectionMustBeRecord"),
             };
 
-            let selection_val = selection.eval(env.as_nzenv());
+            let selection_val = selection.eval(env);
             let sel_kts = match selection_val.kind() {
                 ValueKind::RecordType(kts) => kts,
                 _ => return span_err("ProjectionByExprTakesRecordType"),
@@ -782,14 +780,14 @@ pub(crate) fn type_with(env: &TyEnv, hir: &Hir) -> Result<TyExpr, TypeError> {
             let ekind = match ekind {
                 ExprKind::Lam(binder, annot, body) => {
                     let annot = type_with(env, annot)?;
-                    let annot_nf = annot.eval(env.as_nzenv());
+                    let annot_nf = annot.eval(env);
                     let body_env = env.insert_type(binder, annot_nf);
                     let body = type_with(&body_env, body)?;
                     ExprKind::Lam(binder.clone(), annot, body)
                 }
                 ExprKind::Pi(binder, annot, body) => {
                     let annot = type_with(env, annot)?;
-                    let annot_nf = annot.eval(env.as_nzenv());
+                    let annot_nf = annot.eval(env);
                     let body_env = env.insert_type(binder, annot_nf);
                     let body = type_with(&body_env, body)?;
                     ExprKind::Pi(binder.clone(), annot, body)
@@ -808,7 +806,7 @@ pub(crate) fn type_with(env: &TyEnv, hir: &Hir) -> Result<TyExpr, TypeError> {
                     };
                     let val = type_with(env, &val)?;
                     let val_ty = val.get_type()?;
-                    let val_nf = val.eval(&env.as_nzenv());
+                    let val_nf = val.eval(env);
                     let body_env = env.insert_value(&binder, val_nf, val_ty);
                     let body = type_with(&body_env, body)?;
                     ExprKind::Let(binder.clone(), None, val, body)
-- 
cgit v1.2.3


From 35cc98dc767247f4881866de40c7d8dd82eba8a5 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 9 Feb 2020 22:30:32 +0000
Subject: Remove types from NzEnv

---
 dhall/src/semantics/tck/env.rs    | 14 +++++++-------
 dhall/src/semantics/tck/tyexpr.rs |  4 ++--
 2 files changed, 9 insertions(+), 9 deletions(-)

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

diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index ba7fb73..7990059 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -1,4 +1,4 @@
-use crate::semantics::{AlphaVar, NzEnv, NzVar, Type, Value};
+use crate::semantics::{AlphaVar, NzEnv, NzVar, Type, ValEnv, Value};
 use crate::syntax::{Label, V};
 
 /// Environment for indexing variables.
@@ -17,7 +17,7 @@ pub(crate) struct NameEnv {
 #[derive(Debug, Clone)]
 pub(crate) struct TyEnv {
     names: NameEnv,
-    items: NzEnv,
+    items: ValEnv<Type>,
 }
 
 impl VarEnv {
@@ -91,14 +91,14 @@ impl TyEnv {
     pub fn new() -> Self {
         TyEnv {
             names: NameEnv::new(),
-            items: NzEnv::new(),
+            items: ValEnv::new(),
         }
     }
     pub fn as_varenv(&self) -> VarEnv {
         self.names.as_varenv()
     }
-    pub fn as_nzenv(&self) -> &NzEnv {
-        &self.items
+    pub fn to_nzenv(&self) -> NzEnv {
+        self.items.discard_types()
     }
     pub fn as_nameenv(&self) -> &NameEnv {
         &self.names
@@ -121,8 +121,8 @@ impl TyEnv {
     }
 }
 
-impl<'a> From<&'a TyEnv> for &'a NzEnv {
+impl<'a> From<&'a TyEnv> for NzEnv {
     fn from(x: &'a TyEnv) -> Self {
-        x.as_nzenv()
+        x.to_nzenv()
     }
 }
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index edba477..a1666a4 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -56,13 +56,13 @@ impl TyExpr {
     }
 
     /// Eval the TyExpr. It will actually get evaluated only as needed on demand.
-    pub fn eval<'e>(&self, env: impl Into<&'e NzEnv>) -> Value {
+    pub fn eval(&self, env: impl Into<NzEnv>) -> Value {
         Value::new_thunk(env.into(), self.to_hir())
     }
     /// Eval a closed TyExpr (i.e. without free variables). It will actually get evaluated only as
     /// needed on demand.
     pub fn eval_closed_expr(&self) -> Value {
-        self.eval(&NzEnv::new())
+        self.eval(NzEnv::new())
     }
     /// Eval a closed TyExpr fully and recursively;
     pub fn rec_eval_closed_expr(&self) -> Value {
-- 
cgit v1.2.3


From c3ed75dc4b354becac0821e4288105dc2a300c4c Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 10 Feb 2020 19:14:07 +0000
Subject: Remove need for Embed

This was an archaic leftover from copying the Haskell datatypes anyway
---
 dhall/src/semantics/tck/typecheck.rs | 10 +---------
 1 file changed, 1 insertion(+), 9 deletions(-)

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

diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 7f02832..4e45637 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -761,21 +761,13 @@ fn type_one_layer(
 /// `type_with` typechecks an expressio in the provided environment.
 pub(crate) fn type_with(env: &TyEnv, hir: &Hir) -> Result<TyExpr, TypeError> {
     let (tyekind, ty) = match hir.kind() {
-        HirKind::Var(var) => (TyExprKind::Var(*var), Some(env.lookup(&var))),
+        HirKind::Var(var) => (TyExprKind::Var(*var), Some(env.lookup(var))),
         HirKind::Expr(ExprKind::Var(_)) => {
             unreachable!("Hir should contain no unresolved variables")
         }
         HirKind::Expr(ExprKind::Const(Const::Sort)) => {
             (TyExprKind::Expr(ExprKind::Const(Const::Sort)), None)
         }
-        HirKind::Expr(ExprKind::Embed(p)) => {
-            let val = p.clone().into_value();
-            (
-                val.to_tyexpr_noenv().kind().clone(),
-                Some(val.get_type(&TyEnv::new())?),
-            )
-            // return Ok(p.clone().into_value().to_tyexpr_noenv())
-        }
         HirKind::Expr(ekind) => {
             let ekind = match ekind {
                 ExprKind::Lam(binder, annot, body) => {
-- 
cgit v1.2.3


From 5a2538d174fd36a8ed7f4fa344b9583fc48bd977 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 11 Feb 2020 13:12:13 +0000
Subject: Remove the Embed variant from ExprKind

---
 dhall/src/semantics/tck/tyexpr.rs    | 3 +--
 dhall/src/semantics/tck/typecheck.rs | 7 ++-----
 2 files changed, 3 insertions(+), 7 deletions(-)

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

diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index a1666a4..d46ab87 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,7 +1,6 @@
 use crate::error::{TypeError, TypeMessage};
 use crate::semantics::{AlphaVar, Hir, HirKind, NzEnv, Value};
 use crate::syntax::{ExprKind, Span};
-use crate::Normalized;
 use crate::{NormalizedExpr, ToExprOptions};
 
 pub(crate) type Type = Value;
@@ -10,7 +9,7 @@ pub(crate) type Type = Value;
 pub(crate) enum TyExprKind {
     Var(AlphaVar),
     // Forbidden ExprKind variants: Var, Import, Embed
-    Expr(ExprKind<TyExpr, Normalized>),
+    Expr(ExprKind<TyExpr>),
 }
 
 // An expression with inferred types at every node and resolved variables.
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 4e45637..f9ff3d3 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -11,7 +11,6 @@ use crate::semantics::{
 use crate::syntax::{
     BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Span,
 };
-use crate::Normalized;
 
 fn type_of_recordtype<'a>(
     span: Span,
@@ -51,7 +50,7 @@ pub fn mkerr<T, S: ToString>(x: S) -> Result<T, TypeError> {
 /// layer.
 fn type_one_layer(
     env: &TyEnv,
-    ekind: ExprKind<TyExpr, Normalized>,
+    ekind: ExprKind<TyExpr>,
     span: Span,
 ) -> Result<TyExpr, TypeError> {
     let span_err = |msg: &str| {
@@ -66,9 +65,7 @@ fn type_one_layer(
         ExprKind::Import(..) => unreachable!(
             "There should remain no imports in a resolved expression"
         ),
-        ExprKind::Var(..)
-        | ExprKind::Const(Const::Sort)
-        | ExprKind::Embed(..) => unreachable!(), // Handled in type_with
+        ExprKind::Var(..) | ExprKind::Const(Const::Sort) => unreachable!(), // Handled in type_with
 
         ExprKind::Lam(binder, annot, body) => {
             let body_ty = body.get_type()?;
-- 
cgit v1.2.3


From 40bee3cdcb9ac0c76996feeceb6ca160a6bd8b42 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 11 Feb 2020 19:04:44 +0000
Subject: Introduce LitKind to factor out common enum nodes

---
 dhall/src/semantics/tck/typecheck.rs | 16 +++++++++++-----
 1 file changed, 11 insertions(+), 5 deletions(-)

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

diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index f9ff3d3..c52cfda 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -9,7 +9,7 @@ use crate::semantics::{
     TyExpr, TyExprKind, Type, Value, ValueKind,
 };
 use crate::syntax::{
-    BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Span,
+    BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, LitKind, Span,
 };
 
 fn type_of_recordtype<'a>(
@@ -115,10 +115,16 @@ fn type_one_layer(
             let t_tyexpr = typecheck(&t_hir)?;
             t_tyexpr.eval(env)
         }
-        ExprKind::BoolLit(_) => Value::from_builtin(Builtin::Bool),
-        ExprKind::NaturalLit(_) => Value::from_builtin(Builtin::Natural),
-        ExprKind::IntegerLit(_) => Value::from_builtin(Builtin::Integer),
-        ExprKind::DoubleLit(_) => Value::from_builtin(Builtin::Double),
+        ExprKind::Lit(LitKind::Bool(_)) => Value::from_builtin(Builtin::Bool),
+        ExprKind::Lit(LitKind::Natural(_)) => {
+            Value::from_builtin(Builtin::Natural)
+        }
+        ExprKind::Lit(LitKind::Integer(_)) => {
+            Value::from_builtin(Builtin::Integer)
+        }
+        ExprKind::Lit(LitKind::Double(_)) => {
+            Value::from_builtin(Builtin::Double)
+        }
         ExprKind::TextLit(interpolated) => {
             let text_type = Value::from_builtin(Builtin::Text);
             for contents in interpolated.iter() {
-- 
cgit v1.2.3


From 7b649b8647c60f1c02050805520f307edff0a94f Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 13 Feb 2020 19:48:11 +0000
Subject: Only store type at root node in tyexpr

---
 dhall/src/semantics/tck/tyexpr.rs    | 43 +++++++++++++++---------------------
 dhall/src/semantics/tck/typecheck.rs | 12 ++++++----
 2 files changed, 26 insertions(+), 29 deletions(-)

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

diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index d46ab87..b49ea3e 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,39 +1,30 @@
 use crate::error::{TypeError, TypeMessage};
-use crate::semantics::{AlphaVar, Hir, HirKind, NzEnv, Value};
-use crate::syntax::{ExprKind, Span};
+use crate::semantics::{Hir, HirKind, NzEnv, Value,TyEnv};
+use crate::syntax::Span;
 use crate::{NormalizedExpr, ToExprOptions};
 
 pub(crate) type Type = Value;
 
-#[derive(Debug, Clone)]
-pub(crate) enum TyExprKind {
-    Var(AlphaVar),
-    // Forbidden ExprKind variants: Var, Import, Embed
-    Expr(ExprKind<TyExpr>),
-}
-
-// An expression with inferred types at every node and resolved variables.
+// A hir expression plus its inferred type.
 #[derive(Clone)]
 pub(crate) struct TyExpr {
-    kind: Box<TyExprKind>,
+    hir: Hir,
     ty: Option<Type>,
-    span: Span,
 }
 
 impl TyExpr {
-    pub fn new(kind: TyExprKind, ty: Option<Type>, span: Span) -> Self {
+    pub fn new(kind: HirKind, ty: Option<Type>, span: Span) -> Self {
         TyExpr {
-            kind: Box::new(kind),
+            hir: Hir::new(kind, span),
             ty,
-            span,
         }
     }
 
-    pub fn kind(&self) -> &TyExprKind {
-        &*self.kind
+    pub fn kind(&self) -> &HirKind {
+        self.hir.kind()
     }
     pub fn span(&self) -> Span {
-        self.span.clone()
+        self.as_hir().span()
     }
     pub fn get_type(&self) -> Result<Type, TypeError> {
         match &self.ty {
@@ -41,22 +32,24 @@ impl TyExpr {
             None => Err(TypeError::new(TypeMessage::Sort)),
         }
     }
+    pub fn get_type_tyexpr(&self, env: &TyEnv) -> Result<TyExpr, TypeError> {
+        Ok(self.get_type()?.to_tyexpr_tyenv(env))
+    }
 
     pub fn to_hir(&self) -> Hir {
-        let kind = match self.kind() {
-            TyExprKind::Var(v) => HirKind::Var(v.clone()),
-            TyExprKind::Expr(e) => HirKind::Expr(e.map_ref(|tye| tye.to_hir())),
-        };
-        Hir::new(kind, self.span())
+        self.as_hir().clone()
+    }
+    pub fn as_hir(&self) -> &Hir {
+        &self.hir
     }
     /// Converts a value back to the corresponding AST expression.
     pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
-        self.to_hir().to_expr(opts)
+        self.as_hir().to_expr(opts)
     }
 
     /// Eval the TyExpr. It will actually get evaluated only as needed on demand.
     pub fn eval(&self, env: impl Into<NzEnv>) -> Value {
-        Value::new_thunk(env.into(), self.to_hir())
+        self.as_hir().eval(&env.into())
     }
     /// Eval a closed TyExpr (i.e. without free variables). It will actually get evaluated only as
     /// needed on demand.
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index c52cfda..c854552 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -6,7 +6,7 @@ use crate::error::{ErrorBuilder, TypeError, TypeMessage};
 use crate::semantics::merge_maps;
 use crate::semantics::{
     type_of_builtin, Binder, BuiltinClosure, Closure, Hir, HirKind, TyEnv,
-    TyExpr, TyExprKind, Type, Value, ValueKind,
+    TyExpr, Type, Value, ValueKind,
 };
 use crate::syntax::{
     BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, LitKind, Span,
@@ -758,18 +758,22 @@ fn type_one_layer(
         }
     };
 
-    Ok(TyExpr::new(TyExprKind::Expr(ekind), Some(ty), span))
+    Ok(TyExpr::new(
+        HirKind::Expr(ekind.map_ref(|tye| tye.to_hir())),
+        Some(ty),
+        span,
+    ))
 }
 
 /// `type_with` typechecks an expressio in the provided environment.
 pub(crate) fn type_with(env: &TyEnv, hir: &Hir) -> Result<TyExpr, TypeError> {
     let (tyekind, ty) = match hir.kind() {
-        HirKind::Var(var) => (TyExprKind::Var(*var), Some(env.lookup(var))),
+        HirKind::Var(var) => (HirKind::Var(*var), Some(env.lookup(var))),
         HirKind::Expr(ExprKind::Var(_)) => {
             unreachable!("Hir should contain no unresolved variables")
         }
         HirKind::Expr(ExprKind::Const(Const::Sort)) => {
-            (TyExprKind::Expr(ExprKind::Const(Const::Sort)), None)
+            (HirKind::Expr(ExprKind::Const(Const::Sort)), None)
         }
         HirKind::Expr(ekind) => {
             let ekind = match ekind {
-- 
cgit v1.2.3


From f29a40fb55b898b3a3cc51f198e8522eaecf0777 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 13 Feb 2020 20:17:41 +0000
Subject: Simplify conversions to/from TyExpr

---
 dhall/src/semantics/tck/tyexpr.rs    |  11 ++-
 dhall/src/semantics/tck/typecheck.rs | 157 ++++++++++++++++-------------------
 2 files changed, 78 insertions(+), 90 deletions(-)

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

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


From e25b67906ce68e8726e8139c1d1855f3ab2518ce Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 13 Feb 2020 20:45:42 +0000
Subject: Rework annotation and Sort handling

---
 dhall/src/semantics/tck/typecheck.rs | 143 ++++++++++++++++++-----------------
 1 file changed, 75 insertions(+), 68 deletions(-)

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

diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 794edcf..a4ab31f 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -24,13 +24,10 @@ 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> {
+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())
+            .span_err(span, msg.to_string())
             .format(),
     )
 }
@@ -40,22 +37,25 @@ pub fn mk_span_err<T, S: ToString>(
 fn type_one_layer(
     env: &TyEnv,
     ekind: ExprKind<TyExpr>,
+    annot: Option<Type>,
     span: Span,
 ) -> Result<TyExpr, TypeError> {
-    let span_err = |msg: &str| mk_span_err(&span, msg);
+    let span_err = |msg: &str| mk_span_err(span.clone(), msg);
 
     let ty = match &ekind {
         ExprKind::Import(..) => unreachable!(
             "There should remain no imports in a resolved expression"
         ),
-        ExprKind::Var(..) | ExprKind::Const(Const::Sort) => unreachable!(), // Handled in type_with
+        ExprKind::Var(..)
+        | ExprKind::Const(Const::Sort)
+        | ExprKind::Annot(..) => unreachable!(), // Handled in type_with
 
         ExprKind::Lam(binder, annot, body) => {
             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)
+            type_one_layer(env, pi_ekind, None, Span::Artificial)?.eval(env)
         }
         ExprKind::Pi(_, annot, body) => {
             let ks = match annot.get_type()?.as_const() {
@@ -253,18 +253,6 @@ fn type_one_layer(
                 } // _ => span_err("NotARecord"),
             }
         }
-        ExprKind::Annot(x, t) => {
-            let t = t.eval(env);
-            let x_ty = x.get_type()?;
-            if x_ty != t {
-                return span_err(&format!(
-                    "annot mismatch: {} != {}",
-                    x_ty.to_expr_tyenv(env),
-                    t.to_expr_tyenv(env)
-                ));
-            }
-            x_ty
-        }
         ExprKind::Assert(t) => {
             let t = t.eval(env);
             match &*t.kind() {
@@ -365,7 +353,7 @@ fn type_one_layer(
                 x.get_type_tyexpr(env)?,
                 y.get_type_tyexpr(env)?,
             );
-            type_one_layer(env, ekind, span.clone())?.eval(env)
+            type_one_layer(env, ekind, None, span.clone())?.eval(env)
         }
         ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => {
             fn check_rectymerge(
@@ -376,20 +364,25 @@ fn type_one_layer(
             ) -> Result<(), TypeError> {
                 let kts_x = match x.kind() {
                     ValueKind::RecordType(kts) => kts,
-                    _ => return mk_span_err(span, "RecordTypeMergeRequiresRecordType"),
+                    _ => {
+                        return mk_span_err(
+                            span.clone(),
+                            "RecordTypeMergeRequiresRecordType",
+                        )
+                    }
                 };
                 let kts_y = match y.kind() {
                     ValueKind::RecordType(kts) => kts,
-                    _ => return mk_span_err(span, "RecordTypeMergeRequiresRecordType"),
+                    _ => {
+                        return mk_span_err(
+                            span.clone(),
+                            "RecordTypeMergeRequiresRecordType",
+                        )
+                    }
                 };
                 for (k, tx) in kts_x {
                     if let Some(ty) = kts_y.get(k) {
-                        check_rectymerge(
-                            span,
-                            env,
-                            tx.clone(),
-                            ty.clone(),
-                        )?;
+                        check_rectymerge(span, env, tx.clone(), ty.clone())?;
                     }
                 }
                 Ok(())
@@ -717,30 +710,38 @@ fn type_one_layer(
             let ty_field_default = type_one_layer(
                 env,
                 ExprKind::Field(ty.clone(), "default".into()),
+                None,
                 span.clone(),
             )?;
             let ty_field_type = type_one_layer(
                 env,
                 ExprKind::Field(ty.clone(), "Type".into()),
+                None,
                 span.clone(),
             )?;
-            let merge = type_one_layer(
+            return type_one_layer(
                 env,
                 ExprKind::BinOp(
                     BinOp::RightBiasedRecordMerge,
                     ty_field_default,
                     compl.clone(),
                 ),
-                span.clone(),
-            )?;
-            return type_one_layer(
-                env,
-                ExprKind::Annot(merge, ty_field_type),
+                Some(ty_field_type.eval(env)),
                 span.clone(),
             );
         }
     };
 
+    if let Some(annot) = annot {
+        if ty != annot {
+            return span_err(&format!(
+                "annot mismatch: {} != {}",
+                ty.to_expr_tyenv(env),
+                annot.to_expr_tyenv(env)
+            ));
+        }
+    }
+
     Ok(TyExpr::new(
         HirKind::Expr(ekind.map_ref(|tye| tye.to_hir())),
         Some(ty),
@@ -748,72 +749,78 @@ fn type_one_layer(
     ))
 }
 
-/// `type_with` typechecks an expressio in the provided environment.
-pub(crate) fn type_with(env: &TyEnv, hir: &Hir) -> Result<TyExpr, TypeError> {
-    let (tyekind, ty) = match hir.kind() {
-        HirKind::Var(var) => (HirKind::Var(*var), Some(env.lookup(var))),
+/// `type_with` typechecks an expression in the provided environment. Optionally pass an annotation
+/// to compare with.
+pub(crate) fn type_with(
+    env: &TyEnv,
+    hir: &Hir,
+    annot: Option<Type>,
+) -> Result<TyExpr, TypeError> {
+    match hir.kind() {
+        HirKind::Var(var) => Ok(TyExpr::new(
+            HirKind::Var(*var),
+            Some(env.lookup(var)),
+            hir.span(),
+        )),
         HirKind::Expr(ExprKind::Var(_)) => {
             unreachable!("Hir should contain no unresolved variables")
         }
         HirKind::Expr(ExprKind::Const(Const::Sort)) => {
-            (HirKind::Expr(ExprKind::Const(Const::Sort)), None)
+            mk_span_err(hir.span(), "Sort does not have a type")
+        }
+        HirKind::Expr(ExprKind::Annot(x, t)) => {
+            let t = match t.kind() {
+                HirKind::Expr(ExprKind::Const(Const::Sort)) => {
+                    Value::from_const(Const::Sort)
+                }
+                _ => type_with(env, t, None)?.eval(env),
+            };
+            type_with(env, x, Some(t))
         }
         HirKind::Expr(ekind) => {
             let ekind = match ekind {
                 ExprKind::Lam(binder, annot, body) => {
-                    let annot = type_with(env, annot)?;
+                    let annot = type_with(env, annot, None)?;
                     let annot_nf = annot.eval(env);
                     let body_env = env.insert_type(binder, annot_nf);
-                    let body = type_with(&body_env, body)?;
+                    let body = type_with(&body_env, body, None)?;
                     ExprKind::Lam(binder.clone(), annot, body)
                 }
                 ExprKind::Pi(binder, annot, body) => {
-                    let annot = type_with(env, annot)?;
+                    let annot = type_with(env, annot, None)?;
                     let annot_nf = annot.eval(env);
                     let body_env = env.insert_type(binder, annot_nf);
-                    let body = type_with(&body_env, body)?;
+                    let body = type_with(&body_env, body, None)?;
                     ExprKind::Pi(binder.clone(), annot, body)
                 }
                 ExprKind::Let(binder, annot, val, body) => {
-                    let val = if let Some(t) = annot {
-                        Hir::new(
-                            HirKind::Expr(ExprKind::Annot(
-                                val.clone(),
-                                t.clone(),
-                            )),
-                            t.span(),
-                        )
+                    let val_annot = if let Some(t) = annot {
+                        Some(type_with(env, t, None)?.eval(env))
                     } else {
-                        val.clone()
+                        None
                     };
-                    let val = type_with(env, &val)?;
+                    let val = type_with(env, &val, val_annot)?;
                     let val_ty = val.get_type()?;
                     let val_nf = val.eval(env);
                     let body_env = env.insert_value(&binder, val_nf, val_ty);
-                    let body = type_with(&body_env, body)?;
+                    let body = type_with(&body_env, body, None)?;
                     ExprKind::Let(binder.clone(), None, val, body)
                 }
-                _ => ekind.traverse_ref(|e| type_with(env, e))?,
+                _ => ekind.traverse_ref(|e| type_with(env, e, None))?,
             };
-            return type_one_layer(env, ekind, hir.span());
+            type_one_layer(env, ekind, annot, hir.span())
         }
-    };
-
-    Ok(TyExpr::new(tyekind, ty, hir.span()))
+    }
 }
 
 /// Typecheck an expression and return the expression annotated with types if type-checking
 /// succeeded, or an error if type-checking failed.
-pub(crate) fn typecheck(e: &Hir) -> Result<TyExpr, TypeError> {
-    let res = type_with(&TyEnv::new(), e)?;
-    // Ensure that the inferred type exists (i.e. this is not Sort)
-    res.get_type()?;
-    Ok(res)
+pub(crate) fn typecheck(hir: &Hir) -> Result<TyExpr, TypeError> {
+    type_with(&TyEnv::new(), hir, None)
 }
 
 /// Like `typecheck`, but additionally checks that the expression's type matches the provided type.
 pub(crate) fn typecheck_with(hir: &Hir, ty: Hir) -> Result<TyExpr, TypeError> {
-    let hir =
-        Hir::new(HirKind::Expr(ExprKind::Annot(hir.clone(), ty)), hir.span());
-    typecheck(&hir)
+    let ty = typecheck(&ty)?.eval(&TyEnv::new());
+    type_with(&TyEnv::new(), hir, Some(ty))
 }
-- 
cgit v1.2.3


From 350d1cf7d9c114b1334b2743071b0b99ea64c1ec Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 13 Feb 2020 20:56:38 +0000
Subject: TyExpr always carries a type

---
 dhall/src/semantics/tck/tyexpr.rs    |  41 ++++---------
 dhall/src/semantics/tck/typecheck.rs | 112 +++++++++++++++++------------------
 2 files changed, 67 insertions(+), 86 deletions(-)

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

diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index dc14cd2..ac15ac5 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,4 +1,3 @@
-use crate::error::{TypeError, TypeMessage};
 use crate::semantics::{Hir, HirKind, NzEnv, TyEnv, Value};
 use crate::syntax::{Const, Span};
 use crate::{NormalizedExpr, ToExprOptions};
@@ -6,39 +5,36 @@ use crate::{NormalizedExpr, ToExprOptions};
 pub(crate) type Type = Value;
 
 // A hir expression plus its inferred type.
-#[derive(Clone)]
+#[derive(Debug, Clone)]
 pub(crate) struct TyExpr {
     hir: Hir,
-    ty: Option<Type>,
+    ty: Type,
 }
 
 impl TyExpr {
-    pub fn new(kind: HirKind, ty: Option<Type>, span: Span) -> Self {
+    pub fn new(kind: HirKind, ty: Type, span: Span) -> Self {
         TyExpr {
             hir: Hir::new(kind, span),
             ty,
         }
     }
 
-    pub fn kind(&self) -> &HirKind {
-        self.hir.kind()
-    }
     pub fn span(&self) -> Span {
         self.as_hir().span()
     }
-    pub fn get_type(&self) -> Result<Type, TypeError> {
-        match &self.ty {
-            Some(t) => Ok(t.clone()),
-            None => Err(TypeError::new(TypeMessage::Sort)),
-        }
+    pub fn ty(&self) -> &Type {
+        &self.ty
     }
-    pub fn get_type_tyexpr(&self, env: &TyEnv) -> Result<TyExpr, TypeError> {
-        Ok(self.get_type()?.to_hir(env.as_varenv()).typecheck(env)?)
+    pub fn get_type_tyexpr(&self, env: &TyEnv) -> TyExpr {
+        self.ty()
+            .to_hir(env.as_varenv())
+            .typecheck(env)
+            .expect("Internal type error")
     }
     /// 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 get_kind(&self, env: &TyEnv) -> Option<Const> {
+        self.get_type_tyexpr(env).ty().as_const()
     }
 
     pub fn to_hir(&self) -> Hir {
@@ -68,16 +64,3 @@ impl TyExpr {
         val
     }
 }
-
-impl std::fmt::Debug for TyExpr {
-    fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        let mut x = fmt.debug_struct("TyExpr");
-        x.field("kind", self.kind());
-        if let Some(ty) = self.ty.as_ref() {
-            x.field("type", &ty);
-        } else {
-            x.field("type", &None::<()>);
-        }
-        x.finish()
-    }
-}
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index a4ab31f..b3c9353 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -53,24 +53,24 @@ fn type_one_layer(
         ExprKind::Lam(binder, annot, body) => {
             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, None, Span::Artificial)?.eval(env)
         }
         ExprKind::Pi(_, annot, body) => {
-            let ks = match annot.get_type()?.as_const() {
+            let ks = match annot.ty().as_const() {
                 Some(k) => k,
                 _ => {
                     return mkerr(
                         ErrorBuilder::new(format!(
                             "Invalid input type: `{}`",
-                            annot.get_type()?.to_expr_tyenv(env),
+                            annot.ty().to_expr_tyenv(env),
                         ))
                         .span_err(
                             annot.span(),
                             format!(
                                 "this has type: `{}`",
-                                annot.get_type()?.to_expr_tyenv(env)
+                                annot.ty().to_expr_tyenv(env)
                             ),
                         )
                         .help(format!(
@@ -81,14 +81,14 @@ fn type_one_layer(
                     );
                 }
             };
-            let kt = match body.get_type()?.as_const() {
+            let kt = match body.ty().as_const() {
                 Some(k) => k,
                 _ => return span_err("Invalid output type"),
             };
 
             Value::from_const(function_check(ks, kt))
         }
-        ExprKind::Let(_, _, _, body) => body.get_type()?,
+        ExprKind::Let(_, _, _, body) => body.ty().clone(),
 
         ExprKind::Const(Const::Type) => Value::from_const(Const::Kind),
         ExprKind::Const(Const::Kind) => Value::from_const(Const::Sort),
@@ -112,7 +112,7 @@ fn type_one_layer(
             for contents in interpolated.iter() {
                 use InterpolatedTextContents::Expr;
                 if let Expr(x) = contents {
-                    if x.get_type()? != text_type {
+                    if *x.ty() != text_type {
                         return span_err("InvalidTextInterpolation");
                     }
                 }
@@ -121,7 +121,7 @@ fn type_one_layer(
         }
         ExprKind::EmptyListLit(t) => {
             let t = t.eval(env);
-            match &*t.kind() {
+            match t.kind() {
                 ValueKind::AppliedBuiltin(BuiltinClosure {
                     b: Builtin::List,
                     args,
@@ -135,23 +135,23 @@ fn type_one_layer(
             let mut iter = xs.iter();
             let x = iter.next().unwrap();
             for y in iter {
-                if x.get_type()? != y.get_type()? {
+                if x.ty() != y.ty() {
                     return span_err("InvalidListElement");
                 }
             }
-            if x.get_kind(env)? != Some(Const::Type) {
+            if x.get_kind(env) != Some(Const::Type) {
                 return span_err("InvalidListType");
             }
 
-            let t = x.get_type()?;
+            let t = x.ty().clone();
             Value::from_builtin(Builtin::List).app(t)
         }
         ExprKind::SomeLit(x) => {
-            if x.get_kind(env)? != Some(Const::Type) {
+            if x.get_kind(env) != Some(Const::Type) {
                 return span_err("InvalidOptionalType");
             }
 
-            let t = x.get_type()?;
+            let t = x.ty().clone();
             Value::from_builtin(Builtin::Optional).app(t)
         }
         ExprKind::RecordLit(kvs) => {
@@ -163,11 +163,11 @@ fn type_one_layer(
                     Entry::Occupied(_) => {
                         return span_err("RecordTypeDuplicateField")
                     }
-                    Entry::Vacant(e) => e.insert(v.get_type()?),
+                    Entry::Vacant(e) => e.insert(v.ty().clone()),
                 };
 
                 // Check that the fields have a valid kind
-                match v.get_kind(env)? {
+                match v.get_kind(env) {
                     Some(_) => {}
                     None => return span_err("InvalidFieldType"),
                 }
@@ -191,7 +191,7 @@ fn type_one_layer(
                 };
 
                 // Check the type is a Const and compute final type
-                match t.get_type()?.as_const() {
+                match t.ty().as_const() {
                     Some(c) => k = max(k, c),
                     None => return span_err("InvalidFieldType"),
                 }
@@ -206,7 +206,7 @@ fn type_one_layer(
             let mut k = None;
             for (x, t) in kts {
                 if let Some(t) = t {
-                    match (k, t.get_type()?.as_const()) {
+                    match (k, t.ty().as_const()) {
                         (None, Some(k2)) => k = Some(k2),
                         (Some(k1), Some(k2)) if k1 == k2 => {}
                         _ => return span_err("InvalidFieldType"),
@@ -227,12 +227,12 @@ fn type_one_layer(
             Value::from_const(k)
         }
         ExprKind::Field(scrut, x) => {
-            match &*scrut.get_type()?.kind() {
+            match scrut.ty().kind() {
                 ValueKind::RecordType(kts) => match kts.get(&x) {
                     Some(tth) => tth.clone(),
                     None => return span_err("MissingRecordField"),
                 },
-                // TODO: branch here only when scrut.get_type() is a Const
+                // TODO: branch here only when scrut.ty() is a Const
                 _ => {
                     let scrut_nf = scrut.eval(env);
                     match scrut_nf.kind() {
@@ -255,7 +255,7 @@ fn type_one_layer(
         }
         ExprKind::Assert(t) => {
             let t = t.eval(env);
-            match &*t.kind() {
+            match t.kind() {
                 ValueKind::Equivalence(x, y) if x == y => {}
                 ValueKind::Equivalence(..) => {
                     return span_err("AssertMismatch")
@@ -265,9 +265,9 @@ fn type_one_layer(
             t
         }
         ExprKind::App(f, arg) => {
-            match f.get_type()?.kind() {
+            match f.ty().kind() {
                 ValueKind::PiClosure { annot, closure, .. } => {
-                    if arg.get_type()? != *annot {
+                    if arg.ty() != annot {
                         return mkerr(
                             ErrorBuilder::new(format!(
                                 "wrong type of function argument"
@@ -283,13 +283,13 @@ fn type_one_layer(
                                 arg.span(),
                                 format!(
                                     "but this has type: {}",
-                                    arg.get_type()?.to_expr_tyenv(env),
+                                    arg.ty().to_expr_tyenv(env),
                                 ),
                             )
                             .note(format!(
                                 "expected type `{}`\n   found type `{}`",
                                 annot.to_expr_tyenv(env),
-                                arg.get_type()?.to_expr_tyenv(env),
+                                arg.ty().to_expr_tyenv(env),
                             ))
                             .format(),
                         );
@@ -301,7 +301,7 @@ fn type_one_layer(
                 _ => return mkerr(
                     ErrorBuilder::new(format!(
                         "expected function, found `{}`",
-                        f.get_type()?.to_expr_tyenv(env)
+                        f.ty().to_expr_tyenv(env)
                     ))
                     .span_err(
                         f.span(),
@@ -312,21 +312,21 @@ fn type_one_layer(
             }
         }
         ExprKind::BoolIf(x, y, z) => {
-            if *x.get_type()?.kind() != ValueKind::from_builtin(Builtin::Bool) {
+            if *x.ty().kind() != ValueKind::from_builtin(Builtin::Bool) {
                 return span_err("InvalidPredicate");
             }
-            if y.get_kind(env)? != Some(Const::Type) {
+            if y.get_kind(env) != Some(Const::Type) {
                 return span_err("IfBranchMustBeTerm");
             }
-            if y.get_type()? != z.get_type()? {
+            if y.ty() != z.ty() {
                 return span_err("IfBranchMismatch");
             }
 
-            y.get_type()?
+            y.ty().clone()
         }
         ExprKind::BinOp(BinOp::RightBiasedRecordMerge, x, y) => {
-            let x_type = x.get_type()?;
-            let y_type = y.get_type()?;
+            let x_type = x.ty();
+            let y_type = y.ty();
 
             // Extract the LHS record type
             let kts_x = match x_type.kind() {
@@ -350,8 +350,8 @@ fn type_one_layer(
         ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => {
             let ekind = ExprKind::BinOp(
                 BinOp::RecursiveRecordTypeMerge,
-                x.get_type_tyexpr(env)?,
-                y.get_type_tyexpr(env)?,
+                x.get_type_tyexpr(env),
+                y.get_type_tyexpr(env),
             );
             type_one_layer(env, ekind, None, span.clone())?.eval(env)
         }
@@ -390,13 +390,12 @@ fn type_one_layer(
             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();
-            let yk = y.get_type()?.as_const().unwrap();
+            let xk = x.ty().as_const().unwrap();
+            let yk = y.ty().as_const().unwrap();
             Value::from_const(max(xk, yk))
         }
         ExprKind::BinOp(BinOp::ListAppend, l, r) => {
-            let l_ty = l.get_type()?;
-            match &*l_ty.kind() {
+            match l.ty().kind() {
                 ValueKind::AppliedBuiltin(BuiltinClosure {
                     b: Builtin::List,
                     ..
@@ -404,17 +403,17 @@ fn type_one_layer(
                 _ => return span_err("BinOpTypeMismatch"),
             }
 
-            if l_ty != r.get_type()? {
+            if l.ty() != r.ty() {
                 return span_err("BinOpTypeMismatch");
             }
 
-            l_ty
+            l.ty().clone()
         }
         ExprKind::BinOp(BinOp::Equivalence, l, r) => {
-            if l.get_type()? != r.get_type()? {
+            if l.ty() != r.ty() {
                 return span_err("EquivalenceTypeMismatch");
             }
-            if l.get_kind(env)? != Some(Const::Type) {
+            if l.get_kind(env) != Some(Const::Type) {
                 return span_err("EquivalenceArgumentsMustBeTerms");
             }
 
@@ -436,24 +435,24 @@ fn type_one_layer(
                 BinOp::ImportAlt => unreachable!("ImportAlt leftover in tck"),
             });
 
-            if l.get_type()? != t {
+            if *l.ty() != t {
                 return span_err("BinOpTypeMismatch");
             }
 
-            if r.get_type()? != t {
+            if *r.ty() != t {
                 return span_err("BinOpTypeMismatch");
             }
 
             t
         }
         ExprKind::Merge(record, union, type_annot) => {
-            let record_type = record.get_type()?;
+            let record_type = record.ty();
             let handlers = match record_type.kind() {
                 ValueKind::RecordType(kts) => kts,
                 _ => return span_err("Merge1ArgMustBeRecord"),
             };
 
-            let union_type = union.get_type()?;
+            let union_type = union.ty();
             let variants = match union_type.kind() {
                 ValueKind::UnionType(kts) => Cow::Borrowed(kts),
                 ValueKind::AppliedBuiltin(BuiltinClosure {
@@ -583,10 +582,10 @@ fn type_one_layer(
             }
         }
         ExprKind::ToMap(record, annot) => {
-            if record.get_kind(env)? != Some(Const::Type) {
+            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 record_t = record.ty();
             let kts = match record_t.kind() {
                 ValueKind::RecordType(kts) => kts,
                 _ => {
@@ -656,7 +655,7 @@ fn type_one_layer(
             }
         }
         ExprKind::Projection(record, labels) => {
-            let record_type = record.get_type()?;
+            let record_type = record.ty();
             let kts = match record_type.kind() {
                 ValueKind::RecordType(kts) => kts,
                 _ => return span_err("ProjectionMustBeRecord"),
@@ -681,7 +680,7 @@ fn type_one_layer(
             Value::from_kind(ValueKind::RecordType(new_kts))
         }
         ExprKind::ProjectionByExpr(record, selection) => {
-            let record_type = record.get_type()?;
+            let record_type = record.ty();
             let rec_kts = match record_type.kind() {
                 ValueKind::RecordType(kts) => kts,
                 _ => return span_err("ProjectionMustBeRecord"),
@@ -742,9 +741,10 @@ fn type_one_layer(
         }
     }
 
+    // TODO: avoid retraversing
     Ok(TyExpr::new(
         HirKind::Expr(ekind.map_ref(|tye| tye.to_hir())),
-        Some(ty),
+        ty,
         span,
     ))
 }
@@ -757,11 +757,9 @@ pub(crate) fn type_with(
     annot: Option<Type>,
 ) -> Result<TyExpr, TypeError> {
     match hir.kind() {
-        HirKind::Var(var) => Ok(TyExpr::new(
-            HirKind::Var(*var),
-            Some(env.lookup(var)),
-            hir.span(),
-        )),
+        HirKind::Var(var) => {
+            Ok(TyExpr::new(HirKind::Var(*var), env.lookup(var), hir.span()))
+        }
         HirKind::Expr(ExprKind::Var(_)) => {
             unreachable!("Hir should contain no unresolved variables")
         }
@@ -800,9 +798,9 @@ pub(crate) fn type_with(
                         None
                     };
                     let val = type_with(env, &val, val_annot)?;
-                    let val_ty = val.get_type()?;
                     let val_nf = val.eval(env);
-                    let body_env = env.insert_value(&binder, val_nf, val_ty);
+                    let body_env =
+                        env.insert_value(&binder, val_nf, val.ty().clone());
                     let body = type_with(&body_env, body, None)?;
                     ExprKind::Let(binder.clone(), None, val, body)
                 }
-- 
cgit v1.2.3


From 51cf6a28fa56031dbeae0ff378f0ef84eff7fd3e Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 14 Feb 2020 18:55:27 +0000
Subject: Oops

---
 dhall/src/semantics/tck/tyexpr.rs    | 12 +++++-------
 dhall/src/semantics/tck/typecheck.rs | 18 +++++++++---------
 2 files changed, 14 insertions(+), 16 deletions(-)

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

diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index ac15ac5..c7b8009 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,3 +1,4 @@
+use crate::error::TypeError;
 use crate::semantics::{Hir, HirKind, NzEnv, TyEnv, Value};
 use crate::syntax::{Const, Span};
 use crate::{NormalizedExpr, ToExprOptions};
@@ -25,16 +26,13 @@ impl TyExpr {
     pub fn ty(&self) -> &Type {
         &self.ty
     }
-    pub fn get_type_tyexpr(&self, env: &TyEnv) -> TyExpr {
-        self.ty()
-            .to_hir(env.as_varenv())
-            .typecheck(env)
-            .expect("Internal type error")
+    pub fn get_type_tyexpr(&self, env: &TyEnv) -> Result<TyExpr, TypeError> {
+        Ok(self.ty().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) -> Option<Const> {
-        self.get_type_tyexpr(env).ty().as_const()
+    pub fn get_kind(&self, env: &TyEnv) -> Result<Option<Const>, TypeError> {
+        Ok(self.get_type_tyexpr(env)?.ty().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 b3c9353..377b97e 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -53,7 +53,7 @@ fn type_one_layer(
         ExprKind::Lam(binder, annot, body) => {
             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, None, Span::Artificial)?.eval(env)
         }
@@ -139,7 +139,7 @@ fn type_one_layer(
                     return span_err("InvalidListElement");
                 }
             }
-            if x.get_kind(env) != Some(Const::Type) {
+            if x.get_kind(env)? != Some(Const::Type) {
                 return span_err("InvalidListType");
             }
 
@@ -147,7 +147,7 @@ fn type_one_layer(
             Value::from_builtin(Builtin::List).app(t)
         }
         ExprKind::SomeLit(x) => {
-            if x.get_kind(env) != Some(Const::Type) {
+            if x.get_kind(env)? != Some(Const::Type) {
                 return span_err("InvalidOptionalType");
             }
 
@@ -167,7 +167,7 @@ fn type_one_layer(
                 };
 
                 // Check that the fields have a valid kind
-                match v.get_kind(env) {
+                match v.get_kind(env)? {
                     Some(_) => {}
                     None => return span_err("InvalidFieldType"),
                 }
@@ -315,7 +315,7 @@ fn type_one_layer(
             if *x.ty().kind() != ValueKind::from_builtin(Builtin::Bool) {
                 return span_err("InvalidPredicate");
             }
-            if y.get_kind(env) != Some(Const::Type) {
+            if y.get_kind(env)? != Some(Const::Type) {
                 return span_err("IfBranchMustBeTerm");
             }
             if y.ty() != z.ty() {
@@ -350,8 +350,8 @@ fn type_one_layer(
         ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => {
             let ekind = ExprKind::BinOp(
                 BinOp::RecursiveRecordTypeMerge,
-                x.get_type_tyexpr(env),
-                y.get_type_tyexpr(env),
+                x.get_type_tyexpr(env)?,
+                y.get_type_tyexpr(env)?,
             );
             type_one_layer(env, ekind, None, span.clone())?.eval(env)
         }
@@ -413,7 +413,7 @@ fn type_one_layer(
             if l.ty() != r.ty() {
                 return span_err("EquivalenceTypeMismatch");
             }
-            if l.get_kind(env) != Some(Const::Type) {
+            if l.get_kind(env)? != Some(Const::Type) {
                 return span_err("EquivalenceArgumentsMustBeTerms");
             }
 
@@ -582,7 +582,7 @@ fn type_one_layer(
             }
         }
         ExprKind::ToMap(record, annot) => {
-            if record.get_kind(env) != Some(Const::Type) {
+            if record.get_kind(env)? != Some(Const::Type) {
                 return span_err("`toMap` only accepts records of type `Type`");
             }
             let record_t = record.ty();
-- 
cgit v1.2.3


From d65d639ff93691adbf0a208edb99736003bc64bd Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 15 Feb 2020 19:05:26 +0000
Subject: Factor some tck code to avoid needing get_type_tyexpr

---
 dhall/src/semantics/tck/tyexpr.rs    |  12 ++--
 dhall/src/semantics/tck/typecheck.rs | 118 ++++++++++++++++++++++-------------
 2 files changed, 83 insertions(+), 47 deletions(-)

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

diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index c7b8009..dfb4397 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -26,13 +26,15 @@ impl TyExpr {
     pub fn ty(&self) -> &Type {
         &self.ty
     }
-    pub fn get_type_tyexpr(&self, env: &TyEnv) -> Result<TyExpr, TypeError> {
-        Ok(self.ty().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)?.ty().as_const())
+        Ok(self
+            .ty()
+            .to_hir(env.as_varenv())
+            .typecheck(env)?
+            .ty()
+            .as_const())
     }
 
     pub fn to_hir(&self) -> Hir {
@@ -48,7 +50,7 @@ impl TyExpr {
 
     /// Eval the TyExpr. It will actually get evaluated only as needed on demand.
     pub fn eval(&self, env: impl Into<NzEnv>) -> Value {
-        self.as_hir().eval(&env.into())
+        self.as_hir().eval(env.into())
     }
     /// Eval a closed TyExpr (i.e. without free variables). It will actually get evaluated only as
     /// needed on demand.
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 377b97e..a8a2d95 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -12,6 +12,38 @@ use crate::syntax::{
     BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, LitKind, Span,
 };
 
+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.clone(),
+                "RecordTypeMergeRequiresRecordType",
+            )
+        }
+    };
+    let kts_y = match y.kind() {
+        ValueKind::RecordType(kts) => kts,
+        _ => {
+            return mk_span_err(
+                span.clone(),
+                "RecordTypeMergeRequiresRecordType",
+            )
+        }
+    };
+    for (k, tx) in kts_x {
+        if let Some(ty) = kts_y.get(k) {
+            check_rectymerge(span, env, tx.clone(), ty.clone())?;
+        }
+    }
+    Ok(())
+}
+
 fn function_check(a: Const, b: Const) -> Const {
     if b == Const::Type {
         Const::Type
@@ -51,11 +83,39 @@ fn type_one_layer(
         | ExprKind::Annot(..) => unreachable!(), // Handled in type_with
 
         ExprKind::Lam(binder, annot, body) => {
-            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, None, Span::Artificial)?.eval(env)
+            if annot.ty().as_const().is_none() {
+                return mkerr(
+                    ErrorBuilder::new(format!(
+                        "Invalid input type: `{}`",
+                        annot.ty().to_expr_tyenv(env),
+                    ))
+                    .span_err(
+                        annot.span(),
+                        format!(
+                            "this has type: `{}`",
+                            annot.ty().to_expr_tyenv(env)
+                        ),
+                    )
+                    .help(format!(
+                        "The input type of a function must have type `Type`, \
+                         `Kind` or `Sort`",
+                    ))
+                    .format(),
+                );
+            }
+            let body_env = env.insert_type(&binder, annot.eval(env));
+            if body.get_kind(&body_env)?.is_none() {
+                return span_err("Invalid output type");
+            }
+            Hir::new(
+                HirKind::Expr(ExprKind::Pi(
+                    binder.clone(),
+                    annot.to_hir(),
+                    body.ty().to_hir(body_env.as_varenv()),
+                )),
+                span.clone(),
+            )
+            .eval(env)
         }
         ExprKind::Pi(_, annot, body) => {
             let ks = match annot.ty().as_const() {
@@ -348,45 +408,19 @@ fn type_one_layer(
             Value::from_kind(ValueKind::RecordType(kts))
         }
         ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => {
-            let ekind = ExprKind::BinOp(
-                BinOp::RecursiveRecordTypeMerge,
-                x.get_type_tyexpr(env)?,
-                y.get_type_tyexpr(env)?,
-            );
-            type_one_layer(env, ekind, None, span.clone())?.eval(env)
+            check_rectymerge(&span, env, x.ty().clone(), y.ty().clone())?;
+
+            Hir::new(
+                HirKind::Expr(ExprKind::BinOp(
+                    BinOp::RecursiveRecordTypeMerge,
+                    x.ty().to_hir(env.as_varenv()),
+                    y.ty().to_hir(env.as_varenv()),
+                )),
+                span.clone(),
+            )
+            .eval(env)
         }
         ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => {
-            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.clone(),
-                            "RecordTypeMergeRequiresRecordType",
-                        )
-                    }
-                };
-                let kts_y = match y.kind() {
-                    ValueKind::RecordType(kts) => kts,
-                    _ => {
-                        return mk_span_err(
-                            span.clone(),
-                            "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
-- 
cgit v1.2.3


From 5057144ed99bc4e1a76a0840dd39fc1bd862665c Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 15 Feb 2020 19:10:52 +0000
Subject: Desugar Completion during resolution

---
 dhall/src/semantics/tck/typecheck.rs | 34 ++++++----------------------------
 1 file changed, 6 insertions(+), 28 deletions(-)

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

diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index a8a2d95..36f7173 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -75,12 +75,14 @@ fn type_one_layer(
     let span_err = |msg: &str| mk_span_err(span.clone(), msg);
 
     let ty = match &ekind {
-        ExprKind::Import(..) => unreachable!(
-            "There should remain no imports in a resolved expression"
-        ),
+        ExprKind::Import(..) | ExprKind::Completion(..) => {
+            unreachable!("This case should have been handled in resolution")
+        }
         ExprKind::Var(..)
         | ExprKind::Const(Const::Sort)
-        | ExprKind::Annot(..) => unreachable!(), // Handled in type_with
+        | ExprKind::Annot(..) => {
+            unreachable!("This case should have been handled in type_with")
+        }
 
         ExprKind::Lam(binder, annot, body) => {
             if annot.ty().as_const().is_none() {
@@ -739,30 +741,6 @@ fn type_one_layer(
 
             selection_val
         }
-        ExprKind::Completion(ty, compl) => {
-            let ty_field_default = type_one_layer(
-                env,
-                ExprKind::Field(ty.clone(), "default".into()),
-                None,
-                span.clone(),
-            )?;
-            let ty_field_type = type_one_layer(
-                env,
-                ExprKind::Field(ty.clone(), "Type".into()),
-                None,
-                span.clone(),
-            )?;
-            return type_one_layer(
-                env,
-                ExprKind::BinOp(
-                    BinOp::RightBiasedRecordMerge,
-                    ty_field_default,
-                    compl.clone(),
-                ),
-                Some(ty_field_type.eval(env)),
-                span.clone(),
-            );
-        }
     };
 
     if let Some(annot) = annot {
-- 
cgit v1.2.3


From aa867b21f57f9bef2ec2b9d8450736f9111189ee Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 15 Feb 2020 19:44:40 +0000
Subject: Introduce proper Type struct

---
 dhall/src/semantics/tck/tyexpr.rs    |  54 +++++++++++++++--
 dhall/src/semantics/tck/typecheck.rs | 111 +++++++++++++++++++----------------
 2 files changed, 111 insertions(+), 54 deletions(-)

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

diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index dfb4397..4999899 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,17 +1,53 @@
 use crate::error::TypeError;
-use crate::semantics::{Hir, HirKind, NzEnv, TyEnv, Value};
-use crate::syntax::{Const, Span};
+use crate::semantics::{Hir, HirKind, NzEnv, TyEnv, Value, ValueKind, VarEnv};
+use crate::syntax::{Builtin, Const, Span};
 use crate::{NormalizedExpr, ToExprOptions};
 
-pub(crate) type Type = Value;
+/// An expression representing a type
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub(crate) struct Type {
+    val: Value,
+}
 
-// A hir expression plus its inferred type.
+/// A hir expression plus its inferred type.
 #[derive(Debug, Clone)]
 pub(crate) struct TyExpr {
     hir: Hir,
     ty: Type,
 }
 
+impl Type {
+    pub fn from_const(c: Const) -> Self {
+        Value::from_const(c).into()
+    }
+    pub fn from_builtin(b: Builtin) -> Self {
+        Value::from_builtin(b).into()
+    }
+
+    pub fn to_value(&self) -> Value {
+        self.val.clone()
+    }
+    pub fn as_value(&self) -> &Value {
+        &self.val
+    }
+    pub fn into_value(self) -> Value {
+        self.val
+    }
+    pub fn as_const(&self) -> Option<Const> {
+        self.val.as_const()
+    }
+    pub fn kind(&self) -> &ValueKind {
+        self.val.kind()
+    }
+
+    pub fn to_hir(&self, venv: VarEnv) -> Hir {
+        self.val.to_hir(venv)
+    }
+    pub fn to_expr_tyenv(&self, tyenv: &TyEnv) -> NormalizedExpr {
+        self.val.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv)
+    }
+}
+
 impl TyExpr {
     pub fn new(kind: HirKind, ty: Type, span: Span) -> Self {
         TyExpr {
@@ -52,6 +88,10 @@ impl TyExpr {
     pub fn eval(&self, env: impl Into<NzEnv>) -> Value {
         self.as_hir().eval(env.into())
     }
+    /// Evaluate to a Type.
+    pub fn eval_to_type(&self, env: impl Into<NzEnv>) -> Type {
+        self.eval(env).into()
+    }
     /// Eval a closed TyExpr (i.e. without free variables). It will actually get evaluated only as
     /// needed on demand.
     pub fn eval_closed_expr(&self) -> Value {
@@ -64,3 +104,9 @@ impl TyExpr {
         val
     }
 }
+
+impl From<Value> for Type {
+    fn from(x: Value) -> Type {
+        Type { val: x }
+    }
+}
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 36f7173..dd996ae 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -38,7 +38,8 @@ fn check_rectymerge(
     };
     for (k, tx) in kts_x {
         if let Some(ty) = kts_y.get(k) {
-            check_rectymerge(span, env, tx.clone(), ty.clone())?;
+            // TODO: store Type in RecordType ?
+            check_rectymerge(span, env, tx.clone().into(), ty.clone().into())?;
         }
     }
     Ok(())
@@ -105,7 +106,7 @@ fn type_one_layer(
                     .format(),
                 );
             }
-            let body_env = env.insert_type(&binder, annot.eval(env));
+            let body_env = env.insert_type(&binder, annot.eval_to_type(env));
             if body.get_kind(&body_env)?.is_none() {
                 return span_err("Invalid output type");
             }
@@ -117,7 +118,7 @@ fn type_one_layer(
                 )),
                 span.clone(),
             )
-            .eval(env)
+            .eval_to_type(env)
         }
         ExprKind::Pi(_, annot, body) => {
             let ks = match annot.ty().as_const() {
@@ -148,29 +149,29 @@ fn type_one_layer(
                 _ => return span_err("Invalid output type"),
             };
 
-            Value::from_const(function_check(ks, kt))
+            Type::from_const(function_check(ks, kt))
         }
         ExprKind::Let(_, _, _, body) => body.ty().clone(),
 
-        ExprKind::Const(Const::Type) => Value::from_const(Const::Kind),
-        ExprKind::Const(Const::Kind) => Value::from_const(Const::Sort),
+        ExprKind::Const(Const::Type) => Type::from_const(Const::Kind),
+        ExprKind::Const(Const::Kind) => Type::from_const(Const::Sort),
         ExprKind::Builtin(b) => {
             let t_hir = type_of_builtin(*b);
             let t_tyexpr = typecheck(&t_hir)?;
-            t_tyexpr.eval(env)
+            t_tyexpr.eval_to_type(env)
         }
-        ExprKind::Lit(LitKind::Bool(_)) => Value::from_builtin(Builtin::Bool),
+        ExprKind::Lit(LitKind::Bool(_)) => Type::from_builtin(Builtin::Bool),
         ExprKind::Lit(LitKind::Natural(_)) => {
-            Value::from_builtin(Builtin::Natural)
+            Type::from_builtin(Builtin::Natural)
         }
         ExprKind::Lit(LitKind::Integer(_)) => {
-            Value::from_builtin(Builtin::Integer)
+            Type::from_builtin(Builtin::Integer)
         }
         ExprKind::Lit(LitKind::Double(_)) => {
-            Value::from_builtin(Builtin::Double)
+            Type::from_builtin(Builtin::Double)
         }
         ExprKind::TextLit(interpolated) => {
-            let text_type = Value::from_builtin(Builtin::Text);
+            let text_type = Type::from_builtin(Builtin::Text);
             for contents in interpolated.iter() {
                 use InterpolatedTextContents::Expr;
                 if let Expr(x) = contents {
@@ -182,7 +183,7 @@ fn type_one_layer(
             text_type
         }
         ExprKind::EmptyListLit(t) => {
-            let t = t.eval(env);
+            let t = t.eval_to_type(env);
             match t.kind() {
                 ValueKind::AppliedBuiltin(BuiltinClosure {
                     b: Builtin::List,
@@ -205,16 +206,16 @@ fn type_one_layer(
                 return span_err("InvalidListType");
             }
 
-            let t = x.ty().clone();
-            Value::from_builtin(Builtin::List).app(t)
+            let t = x.ty().to_value();
+            Value::from_builtin(Builtin::List).app(t).to_type()
         }
         ExprKind::SomeLit(x) => {
             if x.get_kind(env)? != Some(Const::Type) {
                 return span_err("InvalidOptionalType");
             }
 
-            let t = x.ty().clone();
-            Value::from_builtin(Builtin::Optional).app(t)
+            let t = x.ty().to_value();
+            Value::from_builtin(Builtin::Optional).app(t).to_type()
         }
         ExprKind::RecordLit(kvs) => {
             use std::collections::hash_map::Entry;
@@ -225,7 +226,7 @@ fn type_one_layer(
                     Entry::Occupied(_) => {
                         return span_err("RecordTypeDuplicateField")
                     }
-                    Entry::Vacant(e) => e.insert(v.ty().clone()),
+                    Entry::Vacant(e) => e.insert(v.ty().to_value()),
                 };
 
                 // Check that the fields have a valid kind
@@ -235,7 +236,7 @@ fn type_one_layer(
                 }
             }
 
-            Value::from_kind(ValueKind::RecordType(kts))
+            Value::from_kind(ValueKind::RecordType(kts)).to_type()
         }
         ExprKind::RecordType(kts) => {
             use std::collections::hash_map::Entry;
@@ -259,7 +260,7 @@ fn type_one_layer(
                 }
             }
 
-            Value::from_const(k)
+            Type::from_const(k)
         }
         ExprKind::UnionType(kts) => {
             use std::collections::hash_map::Entry;
@@ -286,17 +287,17 @@ fn type_one_layer(
             // an union type with only unary variants also has type Type
             let k = k.unwrap_or(Const::Type);
 
-            Value::from_const(k)
+            Type::from_const(k)
         }
         ExprKind::Field(scrut, x) => {
             match scrut.ty().kind() {
                 ValueKind::RecordType(kts) => match kts.get(&x) {
-                    Some(tth) => tth.clone(),
+                    Some(val) => val.clone().to_type(),
                     None => return span_err("MissingRecordField"),
                 },
                 // TODO: branch here only when scrut.ty() is a Const
                 _ => {
-                    let scrut_nf = scrut.eval(env);
+                    let scrut_nf = scrut.eval_to_type(env);
                     match scrut_nf.kind() {
                         ValueKind::UnionType(kts) => match kts.get(x) {
                             // Constructor has type T -> < x: T, ... >
@@ -304,8 +305,11 @@ fn type_one_layer(
                                 Value::from_kind(ValueKind::PiClosure {
                                     binder: Binder::new(x.clone()),
                                     annot: ty.clone(),
-                                    closure: Closure::new_constant(scrut_nf),
+                                    closure: Closure::new_constant(
+                                        scrut_nf.into_value(),
+                                    ),
                                 })
+                                .to_type()
                             }
                             Some(None) => scrut_nf,
                             None => return span_err("MissingUnionField"),
@@ -316,7 +320,7 @@ fn type_one_layer(
             }
         }
         ExprKind::Assert(t) => {
-            let t = t.eval(env);
+            let t = t.eval_to_type(env);
             match t.kind() {
                 ValueKind::Equivalence(x, y) if x == y => {}
                 ValueKind::Equivalence(..) => {
@@ -328,8 +332,9 @@ fn type_one_layer(
         }
         ExprKind::App(f, arg) => {
             match f.ty().kind() {
+                // TODO: store Type in closure
                 ValueKind::PiClosure { annot, closure, .. } => {
-                    if arg.ty() != annot {
+                    if arg.ty().as_value() != annot {
                         return mkerr(
                             ErrorBuilder::new(format!(
                                 "wrong type of function argument"
@@ -358,7 +363,7 @@ fn type_one_layer(
                     }
 
                     let arg_nf = arg.eval(env);
-                    closure.apply(arg_nf)
+                    closure.apply(arg_nf).to_type()
                 }
                 _ => return mkerr(
                     ErrorBuilder::new(format!(
@@ -407,7 +412,7 @@ fn type_one_layer(
                 Ok(r_t.clone())
             })?;
 
-            Value::from_kind(ValueKind::RecordType(kts))
+            Value::from_kind(ValueKind::RecordType(kts)).to_type()
         }
         ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => {
             check_rectymerge(&span, env, x.ty().clone(), y.ty().clone())?;
@@ -420,15 +425,20 @@ fn type_one_layer(
                 )),
                 span.clone(),
             )
-            .eval(env)
+            .eval_to_type(env)
         }
         ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => {
-            check_rectymerge(&span, env, x.eval(env), y.eval(env))?;
+            check_rectymerge(
+                &span,
+                env,
+                x.eval_to_type(env),
+                y.eval_to_type(env),
+            )?;
 
             // A RecordType's type is always a const
             let xk = x.ty().as_const().unwrap();
             let yk = y.ty().as_const().unwrap();
-            Value::from_const(max(xk, yk))
+            Type::from_const(max(xk, yk))
         }
         ExprKind::BinOp(BinOp::ListAppend, l, r) => {
             match l.ty().kind() {
@@ -453,10 +463,10 @@ fn type_one_layer(
                 return span_err("EquivalenceArgumentsMustBeTerms");
             }
 
-            Value::from_const(Const::Type)
+            Type::from_const(Const::Type)
         }
         ExprKind::BinOp(o, l, r) => {
-            let t = Value::from_builtin(match o {
+            let t = Type::from_builtin(match o {
                 BinOp::BoolAnd
                 | BinOp::BoolOr
                 | BinOp::BoolEQ
@@ -507,7 +517,7 @@ fn type_one_layer(
 
             let mut inferred_type = None;
             for (x, handler_type) in handlers {
-                let handler_return_type = match variants.get(x) {
+                let handler_return_type: Type = match variants.get(x) {
                     // Union alternative with type
                     Some(Some(variant_type)) => match handler_type.kind() {
                         ValueKind::PiClosure { closure, annot, .. } => {
@@ -542,7 +552,7 @@ fn type_one_layer(
                             }
 
                             match closure.remove_binder() {
-                                Ok(v) => v,
+                                Ok(v) => v.to_type(),
                                 Err(()) => {
                                     return span_err(
                                         "MergeReturnTypeIsDependent",
@@ -586,7 +596,7 @@ fn type_one_layer(
                         }
                     },
                     // Union alternative without type
-                    Some(None) => handler_type.clone(),
+                    Some(None) => handler_type.clone().to_type(),
                     None => return span_err("MergeHandlerMissingVariant"),
                 };
                 match &inferred_type {
@@ -604,7 +614,7 @@ fn type_one_layer(
                 }
             }
 
-            let type_annot = type_annot.as_ref().map(|t| t.eval(env));
+            let type_annot = type_annot.as_ref().map(|t| t.eval_to_type(env));
             match (inferred_type, type_annot) {
                 (Some(t1), Some(t2)) => {
                     if t1 != t2 {
@@ -638,7 +648,7 @@ fn type_one_layer(
                          annotation",
                     );
                 };
-                let annot_val = annot.eval(env);
+                let annot_val = annot.eval_to_type(env);
 
                 let err_msg = "The type of `toMap x` must be of the form \
                                `List { mapKey : Text, mapValue : T }`";
@@ -679,10 +689,11 @@ fn type_one_layer(
                 let mut kts = HashMap::new();
                 kts.insert("mapKey".into(), Value::from_builtin(Builtin::Text));
                 kts.insert("mapValue".into(), entry_type);
-                let output_type = Value::from_builtin(Builtin::List)
-                    .app(Value::from_kind(ValueKind::RecordType(kts)));
+                let output_type: Type = Value::from_builtin(Builtin::List)
+                    .app(Value::from_kind(ValueKind::RecordType(kts)))
+                    .to_type();
                 if let Some(annot) = annot {
-                    let annot_val = annot.eval(env);
+                    let annot_val = annot.eval_to_type(env);
                     if output_type != annot_val {
                         return span_err("Annotation mismatch");
                     }
@@ -713,7 +724,7 @@ fn type_one_layer(
                 };
             }
 
-            Value::from_kind(ValueKind::RecordType(new_kts))
+            Value::from_kind(ValueKind::RecordType(new_kts)).to_type()
         }
         ExprKind::ProjectionByExpr(record, selection) => {
             let record_type = record.ty();
@@ -722,7 +733,7 @@ fn type_one_layer(
                 _ => return span_err("ProjectionMustBeRecord"),
             };
 
-            let selection_val = selection.eval(env);
+            let selection_val = selection.eval_to_type(env);
             let sel_kts = match selection_val.kind() {
                 ValueKind::RecordType(kts) => kts,
                 _ => return span_err("ProjectionByExprTakesRecordType"),
@@ -781,9 +792,9 @@ pub(crate) fn type_with(
         HirKind::Expr(ExprKind::Annot(x, t)) => {
             let t = match t.kind() {
                 HirKind::Expr(ExprKind::Const(Const::Sort)) => {
-                    Value::from_const(Const::Sort)
+                    Type::from_const(Const::Sort)
                 }
-                _ => type_with(env, t, None)?.eval(env),
+                _ => type_with(env, t, None)?.eval_to_type(env),
             };
             type_with(env, x, Some(t))
         }
@@ -791,21 +802,21 @@ pub(crate) fn type_with(
             let ekind = match ekind {
                 ExprKind::Lam(binder, annot, body) => {
                     let annot = type_with(env, annot, None)?;
-                    let annot_nf = annot.eval(env);
+                    let annot_nf = annot.eval_to_type(env);
                     let body_env = env.insert_type(binder, annot_nf);
                     let body = type_with(&body_env, body, None)?;
                     ExprKind::Lam(binder.clone(), annot, body)
                 }
                 ExprKind::Pi(binder, annot, body) => {
                     let annot = type_with(env, annot, None)?;
-                    let annot_nf = annot.eval(env);
-                    let body_env = env.insert_type(binder, annot_nf);
+                    let annot_val = annot.eval_to_type(env);
+                    let body_env = env.insert_type(binder, annot_val);
                     let body = type_with(&body_env, body, None)?;
                     ExprKind::Pi(binder.clone(), annot, body)
                 }
                 ExprKind::Let(binder, annot, val, body) => {
                     let val_annot = if let Some(t) = annot {
-                        Some(type_with(env, t, None)?.eval(env))
+                        Some(type_with(env, t, None)?.eval_to_type(env))
                     } else {
                         None
                     };
@@ -831,6 +842,6 @@ pub(crate) fn typecheck(hir: &Hir) -> Result<TyExpr, TypeError> {
 
 /// Like `typecheck`, but additionally checks that the expression's type matches the provided type.
 pub(crate) fn typecheck_with(hir: &Hir, ty: Hir) -> Result<TyExpr, TypeError> {
-    let ty = typecheck(&ty)?.eval(&TyEnv::new());
+    let ty = typecheck(&ty)?.eval_to_type(&TyEnv::new());
     type_with(&TyEnv::new(), hir, Some(ty))
 }
-- 
cgit v1.2.3


From 130de8cea49c848a06174c61c747d9414a5c71b7 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 16 Feb 2020 19:06:23 +0000
Subject: Start requiring Universe to build a Type

---
 dhall/src/semantics/tck/tyexpr.rs    | 117 +++++++++++++---
 dhall/src/semantics/tck/typecheck.rs | 263 ++++++++++++++---------------------
 2 files changed, 205 insertions(+), 175 deletions(-)

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

diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index 4999899..3c47a81 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,8 +1,12 @@
-use crate::error::TypeError;
-use crate::semantics::{Hir, HirKind, NzEnv, TyEnv, Value, ValueKind, VarEnv};
+use crate::error::{ErrorBuilder, TypeError};
+use crate::semantics::{mkerr, Hir, NzEnv, TyEnv, Value, ValueKind, VarEnv};
 use crate::syntax::{Builtin, Const, Span};
 use crate::{NormalizedExpr, ToExprOptions};
 
+/// The type of a type. 0 is `Type`, 1 is `Kind`, etc...
+#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Default)]
+pub(crate) struct Universe(u8);
+
 /// An expression representing a type
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub(crate) struct Type {
@@ -16,12 +20,64 @@ pub(crate) struct TyExpr {
     ty: Type,
 }
 
+impl Universe {
+    pub fn from_const(c: Const) -> Self {
+        Universe(match c {
+            Const::Type => 0,
+            Const::Kind => 1,
+            Const::Sort => 2,
+        })
+    }
+    pub fn as_const(self) -> Option<Const> {
+        match self.0 {
+            0 => Some(Const::Type),
+            1 => Some(Const::Kind),
+            2 => Some(Const::Sort),
+            _ => None,
+        }
+    }
+    pub fn next(self) -> Self {
+        Universe(self.0 + 1)
+    }
+    pub fn previous(self) -> Option<Self> {
+        if self.0 == 0 {
+            None
+        } else {
+            Some(Universe(self.0 - 1))
+        }
+    }
+}
+
 impl Type {
+    pub fn new(val: Value, _u: Universe) -> Self {
+        Type { val }
+    }
     pub fn from_const(c: Const) -> Self {
-        Value::from_const(c).into()
+        Self::new(Value::from_const(c), c.to_universe().next())
     }
     pub fn from_builtin(b: Builtin) -> Self {
-        Value::from_builtin(b).into()
+        use Builtin::*;
+        match b {
+            Bool | Natural | Integer | Double | Text => {}
+            _ => unreachable!("this builtin is not a type: {}", b),
+        }
+
+        Self::new(Value::from_builtin(b), Universe::from_const(Const::Type))
+    }
+
+    /// Get the type of this type
+    // TODO: avoid recomputing so much
+    pub fn ty(&self, env: &TyEnv) -> Result<Option<Const>, TypeError> {
+        Ok(self.to_hir(env.as_varenv()).typecheck(env)?.ty().as_const())
+    }
+    /// Get the type of this type
+    // TODO: avoid recomputing so much
+    pub fn ty_univ(&self, env: &TyEnv) -> Result<Universe, TypeError> {
+        Ok(match self.ty(env)? {
+            Some(c) => c.to_universe(),
+            // TODO: hack, might explode
+            None => Const::Sort.to_universe().next(),
+        })
     }
 
     pub fn to_value(&self) -> Value {
@@ -49,9 +105,9 @@ impl Type {
 }
 
 impl TyExpr {
-    pub fn new(kind: HirKind, ty: Type, span: Span) -> Self {
+    pub fn from_hir(hir: &Hir, ty: Type) -> Self {
         TyExpr {
-            hir: Hir::new(kind, span),
+            hir: hir.clone(),
             ty,
         }
     }
@@ -62,16 +118,6 @@ impl TyExpr {
     pub fn ty(&self) -> &Type {
         &self.ty
     }
-    /// 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
-            .ty()
-            .to_hir(env.as_varenv())
-            .typecheck(env)?
-            .ty()
-            .as_const())
-    }
 
     pub fn to_hir(&self) -> Hir {
         self.as_hir().clone()
@@ -79,18 +125,51 @@ impl TyExpr {
     pub fn as_hir(&self) -> &Hir {
         &self.hir
     }
-    /// Converts a value back to the corresponding AST expression.
+    /// Converts a closed expression back to the corresponding AST expression.
     pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
         self.as_hir().to_expr(opts)
     }
+    pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
+        self.as_hir().to_expr_tyenv(env)
+    }
 
     /// Eval the TyExpr. It will actually get evaluated only as needed on demand.
     pub fn eval(&self, env: impl Into<NzEnv>) -> Value {
         self.as_hir().eval(env.into())
     }
+    pub fn ensure_is_type(&self, env: &TyEnv) -> Result<(), TypeError> {
+        if self.ty().as_const().is_none() {
+            return mkerr(
+                ErrorBuilder::new(format!(
+                    "Expected a type, found: `{}`",
+                    self.to_expr_tyenv(env),
+                ))
+                .span_err(
+                    self.span(),
+                    format!(
+                        "this has type: `{}`",
+                        self.ty().to_expr_tyenv(env)
+                    ),
+                )
+                .help(format!(
+                    "An expression in type position must have type `Type`, \
+                     `Kind` or `Sort`",
+                ))
+                .format(),
+            );
+        }
+        Ok(())
+    }
     /// Evaluate to a Type.
-    pub fn eval_to_type(&self, env: impl Into<NzEnv>) -> Type {
-        self.eval(env).into()
+    pub fn eval_to_type(&self, env: &TyEnv) -> Result<Type, TypeError> {
+        self.ensure_is_type(env)?;
+        Ok(Type::new(
+            self.eval(env),
+            self.ty()
+                .as_const()
+                .expect("case handled in ensure_is_type")
+                .to_universe(),
+        ))
     }
     /// Eval a closed TyExpr (i.e. without free variables). It will actually get evaluated only as
     /// needed on demand.
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index dd996ae..1281045 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -15,8 +15,8 @@ use crate::syntax::{
 fn check_rectymerge(
     span: &Span,
     env: &TyEnv,
-    x: Type,
-    y: Type,
+    x: Value,
+    y: Value,
 ) -> Result<(), TypeError> {
     let kts_x = match x.kind() {
         ValueKind::RecordType(kts) => kts,
@@ -39,7 +39,7 @@ fn check_rectymerge(
     for (k, tx) in kts_x {
         if let Some(ty) = kts_y.get(k) {
             // TODO: store Type in RecordType ?
-            check_rectymerge(span, env, tx.clone().into(), ty.clone().into())?;
+            check_rectymerge(span, env, tx.clone(), ty.clone())?;
         }
     }
     Ok(())
@@ -70,9 +70,8 @@ pub fn mk_span_err<T, S: ToString>(span: Span, msg: S) -> Result<T, TypeError> {
 fn type_one_layer(
     env: &TyEnv,
     ekind: ExprKind<TyExpr>,
-    annot: Option<Type>,
     span: Span,
-) -> Result<TyExpr, TypeError> {
+) -> Result<Type, TypeError> {
     let span_err = |msg: &str| mk_span_err(span.clone(), msg);
 
     let ty = match &ekind {
@@ -81,84 +80,19 @@ fn type_one_layer(
         }
         ExprKind::Var(..)
         | ExprKind::Const(Const::Sort)
+        | ExprKind::Lam(..)
+        | ExprKind::Pi(..)
+        | ExprKind::Let(..)
         | ExprKind::Annot(..) => {
             unreachable!("This case should have been handled in type_with")
         }
 
-        ExprKind::Lam(binder, annot, body) => {
-            if annot.ty().as_const().is_none() {
-                return mkerr(
-                    ErrorBuilder::new(format!(
-                        "Invalid input type: `{}`",
-                        annot.ty().to_expr_tyenv(env),
-                    ))
-                    .span_err(
-                        annot.span(),
-                        format!(
-                            "this has type: `{}`",
-                            annot.ty().to_expr_tyenv(env)
-                        ),
-                    )
-                    .help(format!(
-                        "The input type of a function must have type `Type`, \
-                         `Kind` or `Sort`",
-                    ))
-                    .format(),
-                );
-            }
-            let body_env = env.insert_type(&binder, annot.eval_to_type(env));
-            if body.get_kind(&body_env)?.is_none() {
-                return span_err("Invalid output type");
-            }
-            Hir::new(
-                HirKind::Expr(ExprKind::Pi(
-                    binder.clone(),
-                    annot.to_hir(),
-                    body.ty().to_hir(body_env.as_varenv()),
-                )),
-                span.clone(),
-            )
-            .eval_to_type(env)
-        }
-        ExprKind::Pi(_, annot, body) => {
-            let ks = match annot.ty().as_const() {
-                Some(k) => k,
-                _ => {
-                    return mkerr(
-                        ErrorBuilder::new(format!(
-                            "Invalid input type: `{}`",
-                            annot.ty().to_expr_tyenv(env),
-                        ))
-                        .span_err(
-                            annot.span(),
-                            format!(
-                                "this has type: `{}`",
-                                annot.ty().to_expr_tyenv(env)
-                            ),
-                        )
-                        .help(format!(
-                            "The input type of a function must have type \
-                             `Type`, `Kind` or `Sort`",
-                        ))
-                        .format(),
-                    );
-                }
-            };
-            let kt = match body.ty().as_const() {
-                Some(k) => k,
-                _ => return span_err("Invalid output type"),
-            };
-
-            Type::from_const(function_check(ks, kt))
-        }
-        ExprKind::Let(_, _, _, body) => body.ty().clone(),
-
         ExprKind::Const(Const::Type) => Type::from_const(Const::Kind),
         ExprKind::Const(Const::Kind) => Type::from_const(Const::Sort),
         ExprKind::Builtin(b) => {
             let t_hir = type_of_builtin(*b);
             let t_tyexpr = typecheck(&t_hir)?;
-            t_tyexpr.eval_to_type(env)
+            t_tyexpr.eval_to_type(env)?
         }
         ExprKind::Lit(LitKind::Bool(_)) => Type::from_builtin(Builtin::Bool),
         ExprKind::Lit(LitKind::Natural(_)) => {
@@ -183,7 +117,7 @@ fn type_one_layer(
             text_type
         }
         ExprKind::EmptyListLit(t) => {
-            let t = t.eval_to_type(env);
+            let t = t.eval_to_type(env)?;
             match t.kind() {
                 ValueKind::AppliedBuiltin(BuiltinClosure {
                     b: Builtin::List,
@@ -202,7 +136,7 @@ fn type_one_layer(
                     return span_err("InvalidListElement");
                 }
             }
-            if x.get_kind(env)? != Some(Const::Type) {
+            if x.ty().ty(env)? != Some(Const::Type) {
                 return span_err("InvalidListType");
             }
 
@@ -210,7 +144,7 @@ fn type_one_layer(
             Value::from_builtin(Builtin::List).app(t).to_type()
         }
         ExprKind::SomeLit(x) => {
-            if x.get_kind(env)? != Some(Const::Type) {
+            if x.ty().ty(env)? != Some(Const::Type) {
                 return span_err("InvalidOptionalType");
             }
 
@@ -230,7 +164,7 @@ fn type_one_layer(
                 };
 
                 // Check that the fields have a valid kind
-                match v.get_kind(env)? {
+                match v.ty().ty(env)? {
                     Some(_) => {}
                     None => return span_err("InvalidFieldType"),
                 }
@@ -297,7 +231,7 @@ fn type_one_layer(
                 },
                 // TODO: branch here only when scrut.ty() is a Const
                 _ => {
-                    let scrut_nf = scrut.eval_to_type(env);
+                    let scrut_nf = scrut.eval(env);
                     match scrut_nf.kind() {
                         ValueKind::UnionType(kts) => match kts.get(x) {
                             // Constructor has type T -> < x: T, ... >
@@ -305,13 +239,11 @@ fn type_one_layer(
                                 Value::from_kind(ValueKind::PiClosure {
                                     binder: Binder::new(x.clone()),
                                     annot: ty.clone(),
-                                    closure: Closure::new_constant(
-                                        scrut_nf.into_value(),
-                                    ),
+                                    closure: Closure::new_constant(scrut_nf),
                                 })
                                 .to_type()
                             }
-                            Some(None) => scrut_nf,
+                            Some(None) => scrut_nf.to_type(),
                             None => return span_err("MissingUnionField"),
                         },
                         _ => return span_err("NotARecord"),
@@ -320,7 +252,7 @@ fn type_one_layer(
             }
         }
         ExprKind::Assert(t) => {
-            let t = t.eval_to_type(env);
+            let t = t.eval_to_type(env)?;
             match t.kind() {
                 ValueKind::Equivalence(x, y) if x == y => {}
                 ValueKind::Equivalence(..) => {
@@ -382,7 +314,7 @@ fn type_one_layer(
             if *x.ty().kind() != ValueKind::from_builtin(Builtin::Bool) {
                 return span_err("InvalidPredicate");
             }
-            if y.get_kind(env)? != Some(Const::Type) {
+            if y.ty().ty(env)? != Some(Const::Type) {
                 return span_err("IfBranchMustBeTerm");
             }
             if y.ty() != z.ty() {
@@ -415,25 +347,22 @@ fn type_one_layer(
             Value::from_kind(ValueKind::RecordType(kts)).to_type()
         }
         ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => {
-            check_rectymerge(&span, env, x.ty().clone(), y.ty().clone())?;
+            check_rectymerge(&span, env, x.ty().to_value(), y.ty().to_value())?;
 
-            Hir::new(
+            let hir = Hir::new(
                 HirKind::Expr(ExprKind::BinOp(
                     BinOp::RecursiveRecordTypeMerge,
                     x.ty().to_hir(env.as_varenv()),
                     y.ty().to_hir(env.as_varenv()),
                 )),
                 span.clone(),
-            )
-            .eval_to_type(env)
+            );
+            let x_u = x.ty().ty_univ(env)?;
+            let y_u = y.ty().ty_univ(env)?;
+            Type::new(hir.eval(env), max(x_u, y_u))
         }
         ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => {
-            check_rectymerge(
-                &span,
-                env,
-                x.eval_to_type(env),
-                y.eval_to_type(env),
-            )?;
+            check_rectymerge(&span, env, x.eval(env), y.eval(env))?;
 
             // A RecordType's type is always a const
             let xk = x.ty().as_const().unwrap();
@@ -459,7 +388,7 @@ fn type_one_layer(
             if l.ty() != r.ty() {
                 return span_err("EquivalenceTypeMismatch");
             }
-            if l.get_kind(env)? != Some(Const::Type) {
+            if l.ty().ty(env)? != Some(Const::Type) {
                 return span_err("EquivalenceArgumentsMustBeTerms");
             }
 
@@ -614,7 +543,10 @@ fn type_one_layer(
                 }
             }
 
-            let type_annot = type_annot.as_ref().map(|t| t.eval_to_type(env));
+            let type_annot = type_annot
+                .as_ref()
+                .map(|t| t.eval_to_type(env))
+                .transpose()?;
             match (inferred_type, type_annot) {
                 (Some(t1), Some(t2)) => {
                     if t1 != t2 {
@@ -628,7 +560,7 @@ fn type_one_layer(
             }
         }
         ExprKind::ToMap(record, annot) => {
-            if record.get_kind(env)? != Some(Const::Type) {
+            if record.ty().ty(env)? != Some(Const::Type) {
                 return span_err("`toMap` only accepts records of type `Type`");
             }
             let record_t = record.ty();
@@ -648,7 +580,7 @@ fn type_one_layer(
                          annotation",
                     );
                 };
-                let annot_val = annot.eval_to_type(env);
+                let annot_val = annot.eval_to_type(env)?;
 
                 let err_msg = "The type of `toMap x` must be of the form \
                                `List { mapKey : Text, mapValue : T }`";
@@ -693,7 +625,7 @@ fn type_one_layer(
                     .app(Value::from_kind(ValueKind::RecordType(kts)))
                     .to_type();
                 if let Some(annot) = annot {
-                    let annot_val = annot.eval_to_type(env);
+                    let annot_val = annot.eval_to_type(env)?;
                     if output_type != annot_val {
                         return span_err("Annotation mismatch");
                     }
@@ -733,7 +665,7 @@ fn type_one_layer(
                 _ => return span_err("ProjectionMustBeRecord"),
             };
 
-            let selection_val = selection.eval_to_type(env);
+            let selection_val = selection.eval_to_type(env)?;
             let sel_kts = match selection_val.kind() {
                 ValueKind::RecordType(kts) => kts,
                 _ => return span_err("ProjectionByExprTakesRecordType"),
@@ -754,22 +686,7 @@ fn type_one_layer(
         }
     };
 
-    if let Some(annot) = annot {
-        if ty != annot {
-            return span_err(&format!(
-                "annot mismatch: {} != {}",
-                ty.to_expr_tyenv(env),
-                annot.to_expr_tyenv(env)
-            ));
-        }
-    }
-
-    // TODO: avoid retraversing
-    Ok(TyExpr::new(
-        HirKind::Expr(ekind.map_ref(|tye| tye.to_hir())),
-        ty,
-        span,
-    ))
+    Ok(ty)
 }
 
 /// `type_with` typechecks an expression in the provided environment. Optionally pass an annotation
@@ -779,59 +696,93 @@ pub(crate) fn type_with(
     hir: &Hir,
     annot: Option<Type>,
 ) -> Result<TyExpr, TypeError> {
-    match hir.kind() {
-        HirKind::Var(var) => {
-            Ok(TyExpr::new(HirKind::Var(*var), env.lookup(var), hir.span()))
-        }
+    let tyexpr = match hir.kind() {
+        HirKind::Var(var) => TyExpr::from_hir(hir, env.lookup(var)),
         HirKind::Expr(ExprKind::Var(_)) => {
             unreachable!("Hir should contain no unresolved variables")
         }
         HirKind::Expr(ExprKind::Const(Const::Sort)) => {
-            mk_span_err(hir.span(), "Sort does not have a type")
+            return mk_span_err(hir.span(), "Sort does not have a type")
         }
         HirKind::Expr(ExprKind::Annot(x, t)) => {
             let t = match t.kind() {
                 HirKind::Expr(ExprKind::Const(Const::Sort)) => {
                     Type::from_const(Const::Sort)
                 }
-                _ => type_with(env, t, None)?.eval_to_type(env),
+                _ => type_with(env, t, None)?.eval_to_type(env)?,
             };
-            type_with(env, x, Some(t))
+            type_with(env, x, Some(t))?
         }
-        HirKind::Expr(ekind) => {
-            let ekind = match ekind {
-                ExprKind::Lam(binder, annot, body) => {
-                    let annot = type_with(env, annot, None)?;
-                    let annot_nf = annot.eval_to_type(env);
-                    let body_env = env.insert_type(binder, annot_nf);
-                    let body = type_with(&body_env, body, None)?;
-                    ExprKind::Lam(binder.clone(), annot, body)
-                }
-                ExprKind::Pi(binder, annot, body) => {
-                    let annot = type_with(env, annot, None)?;
-                    let annot_val = annot.eval_to_type(env);
-                    let body_env = env.insert_type(binder, annot_val);
-                    let body = type_with(&body_env, body, None)?;
-                    ExprKind::Pi(binder.clone(), annot, body)
-                }
-                ExprKind::Let(binder, annot, val, body) => {
-                    let val_annot = if let Some(t) = annot {
-                        Some(type_with(env, t, None)?.eval_to_type(env))
-                    } else {
-                        None
-                    };
-                    let val = type_with(env, &val, val_annot)?;
-                    let val_nf = val.eval(env);
-                    let body_env =
-                        env.insert_value(&binder, val_nf, val.ty().clone());
-                    let body = type_with(&body_env, body, None)?;
-                    ExprKind::Let(binder.clone(), None, val, body)
-                }
-                _ => ekind.traverse_ref(|e| type_with(env, e, None))?,
+
+        HirKind::Expr(ExprKind::Lam(binder, annot, body)) => {
+            let annot = type_with(env, annot, None)?;
+            let annot_nf = annot.eval_to_type(env)?;
+            let body_env = env.insert_type(binder, annot_nf);
+            let body = type_with(&body_env, body, None)?;
+
+            let u_annot = annot.ty().as_const().unwrap();
+            let u_body = match body.ty().ty(&body_env)? {
+                Some(k) => k,
+                _ => return mk_span_err(hir.span(), "Invalid output type"),
             };
-            type_one_layer(env, ekind, annot, hir.span())
+            let u = function_check(u_annot, u_body).to_universe();
+            let ty_hir = Hir::new(
+                HirKind::Expr(ExprKind::Pi(
+                    binder.clone(),
+                    annot.to_hir(),
+                    body.ty().to_hir(body_env.as_varenv()),
+                )),
+                hir.span(),
+            );
+            let ty = Type::new(ty_hir.eval(env), u);
+
+            TyExpr::from_hir(hir, ty)
+        }
+        HirKind::Expr(ExprKind::Pi(binder, annot, body)) => {
+            let annot = type_with(env, annot, None)?;
+            let annot_val = annot.eval_to_type(env)?;
+            let body_env = env.insert_type(binder, annot_val);
+            let body = type_with(&body_env, body, None)?;
+            body.ensure_is_type(env)?;
+
+            let ks = annot.ty().as_const().unwrap();
+            let kt = body.ty().as_const().unwrap();
+            let ty = Type::from_const(function_check(ks, kt));
+            TyExpr::from_hir(hir, ty)
+        }
+        HirKind::Expr(ExprKind::Let(binder, annot, val, body)) => {
+            let val_annot = annot
+                .as_ref()
+                .map(|t| Ok(type_with(env, t, None)?.eval_to_type(env)?))
+                .transpose()?;
+            let val = type_with(env, &val, val_annot)?;
+            let val_nf = val.eval(env);
+            let body_env = env.insert_value(&binder, val_nf, val.ty().clone());
+            let body = type_with(&body_env, body, None)?;
+            let ty = body.ty().clone();
+            TyExpr::from_hir(hir, ty)
+        }
+        HirKind::Expr(ekind) => {
+            let ekind = ekind.traverse_ref(|e| type_with(env, e, None))?;
+            let ty = type_one_layer(env, ekind, hir.span())?;
+            TyExpr::from_hir(hir, ty)
+        }
+    };
+
+    if let Some(annot) = annot {
+        if *tyexpr.ty() != annot {
+            return mk_span_err(
+                hir.span(),
+                &format!(
+                    "annot mismatch: {} != {}",
+                    tyexpr.ty().to_expr_tyenv(env),
+                    annot.to_expr_tyenv(env)
+                ),
+            );
         }
     }
+
+    Ok(tyexpr)
 }
 
 /// Typecheck an expression and return the expression annotated with types if type-checking
@@ -842,6 +793,6 @@ pub(crate) fn typecheck(hir: &Hir) -> Result<TyExpr, TypeError> {
 
 /// Like `typecheck`, but additionally checks that the expression's type matches the provided type.
 pub(crate) fn typecheck_with(hir: &Hir, ty: Hir) -> Result<TyExpr, TypeError> {
-    let ty = typecheck(&ty)?.eval_to_type(&TyEnv::new());
+    let ty = typecheck(&ty)?.eval_to_type(&TyEnv::new())?;
     type_with(&TyEnv::new(), hir, Some(ty))
 }
-- 
cgit v1.2.3


From c451c18103b871e563b12c524bc3feec5451154c Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 16 Feb 2020 19:48:35 +0000
Subject: Avoid recomputing universes in tck

---
 dhall/src/semantics/tck/tyexpr.rs    | 49 ++++++++++++------------
 dhall/src/semantics/tck/typecheck.rs | 73 ++++++++++++++++++++++--------------
 2 files changed, 70 insertions(+), 52 deletions(-)

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

diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index 3c47a81..f6591ba 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -11,6 +11,7 @@ pub(crate) struct Universe(u8);
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub(crate) struct Type {
     val: Value,
+    univ: Universe,
 }
 
 /// A hir expression plus its inferred type.
@@ -39,18 +40,28 @@ impl Universe {
     pub fn next(self) -> Self {
         Universe(self.0 + 1)
     }
-    pub fn previous(self) -> Option<Self> {
-        if self.0 == 0 {
-            None
-        } else {
-            Some(Universe(self.0 - 1))
-        }
-    }
 }
 
 impl Type {
-    pub fn new(val: Value, _u: Universe) -> Self {
-        Type { val }
+    pub fn new(val: Value, univ: Universe) -> Self {
+        Type { val, univ }
+    }
+    /// Creates a new Type and infers its universe by re-typechecking its value.
+    /// TODO: ideally avoid this function altogether. Would need to store types in RecordType and
+    /// PiClosure.
+    pub fn new_infer_universe(
+        env: &TyEnv,
+        val: Value,
+    ) -> Result<Self, TypeError> {
+        let c = val.to_hir(env.as_varenv()).typecheck(env)?.ty().as_const();
+        let u = match c {
+            Some(c) => c.to_universe(),
+            None => unreachable!(
+                "internal type error: this is not a type: {:?}",
+                val
+            ),
+        };
+        Ok(Type::new(val, u))
     }
     pub fn from_const(c: Const) -> Self {
         Self::new(Value::from_const(c), c.to_universe().next())
@@ -66,18 +77,8 @@ impl Type {
     }
 
     /// Get the type of this type
-    // TODO: avoid recomputing so much
-    pub fn ty(&self, env: &TyEnv) -> Result<Option<Const>, TypeError> {
-        Ok(self.to_hir(env.as_varenv()).typecheck(env)?.ty().as_const())
-    }
-    /// Get the type of this type
-    // TODO: avoid recomputing so much
-    pub fn ty_univ(&self, env: &TyEnv) -> Result<Universe, TypeError> {
-        Ok(match self.ty(env)? {
-            Some(c) => c.to_universe(),
-            // TODO: hack, might explode
-            None => Const::Sort.to_universe().next(),
-        })
+    pub fn ty(&self) -> Universe {
+        self.univ
     }
 
     pub fn to_value(&self) -> Value {
@@ -184,8 +185,8 @@ impl TyExpr {
     }
 }
 
-impl From<Value> for Type {
-    fn from(x: Value) -> Type {
-        Type { val: x }
+impl From<Const> for Universe {
+    fn from(x: Const) -> Universe {
+        Universe::from_const(x)
     }
 }
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 1281045..45b3168 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -136,24 +136,30 @@ fn type_one_layer(
                     return span_err("InvalidListElement");
                 }
             }
-            if x.ty().ty(env)? != Some(Const::Type) {
+            if x.ty().ty().as_const() != Some(Const::Type) {
                 return span_err("InvalidListType");
             }
 
             let t = x.ty().to_value();
-            Value::from_builtin(Builtin::List).app(t).to_type()
+            Value::from_builtin(Builtin::List)
+                .app(t)
+                .to_type(Const::Type)
         }
         ExprKind::SomeLit(x) => {
-            if x.ty().ty(env)? != Some(Const::Type) {
+            if x.ty().ty().as_const() != Some(Const::Type) {
                 return span_err("InvalidOptionalType");
             }
 
             let t = x.ty().to_value();
-            Value::from_builtin(Builtin::Optional).app(t).to_type()
+            Value::from_builtin(Builtin::Optional)
+                .app(t)
+                .to_type(Const::Type)
         }
         ExprKind::RecordLit(kvs) => {
             use std::collections::hash_map::Entry;
             let mut kts = HashMap::new();
+            // An empty record type has type Type
+            let mut k = Const::Type;
             for (x, v) in kvs {
                 // Check for duplicated entries
                 match kts.entry(x.clone()) {
@@ -164,13 +170,13 @@ fn type_one_layer(
                 };
 
                 // Check that the fields have a valid kind
-                match v.ty().ty(env)? {
-                    Some(_) => {}
+                match v.ty().ty().as_const() {
+                    Some(c) => k = max(k, c),
                     None => return span_err("InvalidFieldType"),
                 }
             }
 
-            Value::from_kind(ValueKind::RecordType(kts)).to_type()
+            Value::from_kind(ValueKind::RecordType(kts)).to_type(k)
         }
         ExprKind::RecordType(kts) => {
             use std::collections::hash_map::Entry;
@@ -226,29 +232,31 @@ fn type_one_layer(
         ExprKind::Field(scrut, x) => {
             match scrut.ty().kind() {
                 ValueKind::RecordType(kts) => match kts.get(&x) {
-                    Some(val) => val.clone().to_type(),
+                    Some(val) => Type::new_infer_universe(env, val.clone())?,
                     None => return span_err("MissingRecordField"),
                 },
-                // TODO: branch here only when scrut.ty() is a Const
-                _ => {
-                    let scrut_nf = scrut.eval(env);
-                    match scrut_nf.kind() {
+                ValueKind::Const(_) => {
+                    let scrut = scrut.eval_to_type(env)?;
+                    match scrut.kind() {
                         ValueKind::UnionType(kts) => match kts.get(x) {
                             // Constructor has type T -> < x: T, ... >
                             Some(Some(ty)) => {
                                 Value::from_kind(ValueKind::PiClosure {
                                     binder: Binder::new(x.clone()),
                                     annot: ty.clone(),
-                                    closure: Closure::new_constant(scrut_nf),
+                                    closure: Closure::new_constant(
+                                        scrut.to_value(),
+                                    ),
                                 })
-                                .to_type()
+                                .to_type(scrut.ty())
                             }
-                            Some(None) => scrut_nf.to_type(),
+                            Some(None) => scrut,
                             None => return span_err("MissingUnionField"),
                         },
                         _ => return span_err("NotARecord"),
                     }
-                } // _ => span_err("NotARecord"),
+                }
+                _ => return span_err("NotARecord"),
             }
         }
         ExprKind::Assert(t) => {
@@ -295,7 +303,7 @@ fn type_one_layer(
                     }
 
                     let arg_nf = arg.eval(env);
-                    closure.apply(arg_nf).to_type()
+                    Type::new_infer_universe(env, closure.apply(arg_nf))?
                 }
                 _ => return mkerr(
                     ErrorBuilder::new(format!(
@@ -314,7 +322,7 @@ fn type_one_layer(
             if *x.ty().kind() != ValueKind::from_builtin(Builtin::Bool) {
                 return span_err("InvalidPredicate");
             }
-            if y.ty().ty(env)? != Some(Const::Type) {
+            if y.ty().ty().as_const() != Some(Const::Type) {
                 return span_err("IfBranchMustBeTerm");
             }
             if y.ty() != z.ty() {
@@ -344,7 +352,8 @@ fn type_one_layer(
                 Ok(r_t.clone())
             })?;
 
-            Value::from_kind(ValueKind::RecordType(kts)).to_type()
+            let u = max(x.ty().ty(), y.ty().ty());
+            Value::from_kind(ValueKind::RecordType(kts)).to_type(u)
         }
         ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => {
             check_rectymerge(&span, env, x.ty().to_value(), y.ty().to_value())?;
@@ -357,8 +366,8 @@ fn type_one_layer(
                 )),
                 span.clone(),
             );
-            let x_u = x.ty().ty_univ(env)?;
-            let y_u = y.ty().ty_univ(env)?;
+            let x_u = x.ty().ty();
+            let y_u = y.ty().ty();
             Type::new(hir.eval(env), max(x_u, y_u))
         }
         ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => {
@@ -388,7 +397,7 @@ fn type_one_layer(
             if l.ty() != r.ty() {
                 return span_err("EquivalenceTypeMismatch");
             }
-            if l.ty().ty(env)? != Some(Const::Type) {
+            if l.ty().ty().as_const() != Some(Const::Type) {
                 return span_err("EquivalenceArgumentsMustBeTerms");
             }
 
@@ -480,8 +489,11 @@ fn type_one_layer(
                                 );
                             }
 
+                            // TODO: this actually doesn't check anything yet
                             match closure.remove_binder() {
-                                Ok(v) => v.to_type(),
+                                Ok(v) => {
+                                    Type::new_infer_universe(env, v.clone())?
+                                }
                                 Err(()) => {
                                     return span_err(
                                         "MergeReturnTypeIsDependent",
@@ -525,7 +537,9 @@ fn type_one_layer(
                         }
                     },
                     // Union alternative without type
-                    Some(None) => handler_type.clone().to_type(),
+                    Some(None) => {
+                        Type::new_infer_universe(env, handler_type.clone())?
+                    }
                     None => return span_err("MergeHandlerMissingVariant"),
                 };
                 match &inferred_type {
@@ -560,7 +574,7 @@ fn type_one_layer(
             }
         }
         ExprKind::ToMap(record, annot) => {
-            if record.ty().ty(env)? != Some(Const::Type) {
+            if record.ty().ty().as_const() != Some(Const::Type) {
                 return span_err("`toMap` only accepts records of type `Type`");
             }
             let record_t = record.ty();
@@ -623,7 +637,7 @@ fn type_one_layer(
                 kts.insert("mapValue".into(), entry_type);
                 let output_type: Type = Value::from_builtin(Builtin::List)
                     .app(Value::from_kind(ValueKind::RecordType(kts)))
-                    .to_type();
+                    .to_type(Const::Type);
                 if let Some(annot) = annot {
                     let annot_val = annot.eval_to_type(env)?;
                     if output_type != annot_val {
@@ -656,7 +670,10 @@ fn type_one_layer(
                 };
             }
 
-            Value::from_kind(ValueKind::RecordType(new_kts)).to_type()
+            Type::new_infer_universe(
+                env,
+                Value::from_kind(ValueKind::RecordType(new_kts)),
+            )?
         }
         ExprKind::ProjectionByExpr(record, selection) => {
             let record_type = record.ty();
@@ -721,7 +738,7 @@ pub(crate) fn type_with(
             let body = type_with(&body_env, body, None)?;
 
             let u_annot = annot.ty().as_const().unwrap();
-            let u_body = match body.ty().ty(&body_env)? {
+            let u_body = match body.ty().ty().as_const() {
                 Some(k) => k,
                 _ => return mk_span_err(hir.span(), "Invalid output type"),
             };
-- 
cgit v1.2.3


From 8da4445e6d06cf79d43112042b69c798f86884f3 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 17 Feb 2020 17:58:03 +0000
Subject: Extract resolve-relevant envs together

---
 dhall/src/semantics/tck/env.rs | 59 ++++--------------------------------------
 1 file changed, 5 insertions(+), 54 deletions(-)

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

diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index 7990059..f290c02 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -1,5 +1,5 @@
-use crate::semantics::{AlphaVar, NzEnv, NzVar, Type, ValEnv, Value};
-use crate::syntax::{Label, V};
+use crate::semantics::{AlphaVar, NameEnv, NzEnv, NzVar, Type, ValEnv, Value};
+use crate::syntax::Label;
 
 /// Environment for indexing variables.
 #[derive(Debug, Clone, Copy)]
@@ -7,12 +7,6 @@ pub(crate) struct VarEnv {
     size: usize,
 }
 
-/// Environment for resolving names.
-#[derive(Debug, Clone)]
-pub(crate) struct NameEnv {
-    names: Vec<Label>,
-}
-
 /// Environment for typing expressions.
 #[derive(Debug, Clone)]
 pub(crate) struct TyEnv {
@@ -24,6 +18,9 @@ impl VarEnv {
     pub fn new() -> Self {
         VarEnv { size: 0 }
     }
+    pub fn from_size(size: usize) -> Self {
+        VarEnv { size }
+    }
     pub fn size(&self) -> usize {
         self.size
     }
@@ -41,52 +38,6 @@ impl VarEnv {
     }
 }
 
-impl NameEnv {
-    pub fn new() -> Self {
-        NameEnv { names: Vec::new() }
-    }
-    pub fn as_varenv(&self) -> VarEnv {
-        VarEnv {
-            size: self.names.len(),
-        }
-    }
-
-    pub fn insert(&self, x: &Label) -> Self {
-        let mut env = self.clone();
-        env.insert_mut(x);
-        env
-    }
-    pub fn insert_mut(&mut self, x: &Label) {
-        self.names.push(x.clone())
-    }
-    pub fn remove_mut(&mut self) {
-        self.names.pop();
-    }
-
-    pub fn unlabel_var(&self, var: &V) -> Option<AlphaVar> {
-        let V(name, idx) = var;
-        let (idx, _) = self
-            .names
-            .iter()
-            .rev()
-            .enumerate()
-            .filter(|(_, n)| *n == name)
-            .nth(*idx)?;
-        Some(AlphaVar::new(idx))
-    }
-    pub fn label_var(&self, var: &AlphaVar) -> V {
-        let name = &self.names[self.names.len() - 1 - var.idx()];
-        let idx = self
-            .names
-            .iter()
-            .rev()
-            .take(var.idx())
-            .filter(|n| *n == name)
-            .count();
-        V(name.clone(), idx)
-    }
-}
-
 impl TyEnv {
     pub fn new() -> Self {
         TyEnv {
-- 
cgit v1.2.3


From 2f65c02a995f6b6d4c755197fc074782f6bb100d Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 17 Feb 2020 18:12:44 +0000
Subject: Rename TyExpr to Tir

---
 dhall/src/semantics/tck/mod.rs       |   4 +-
 dhall/src/semantics/tck/tir.rs       | 193 +++++++++++++++++++++++++++++++++++
 dhall/src/semantics/tck/tyexpr.rs    | 192 ----------------------------------
 dhall/src/semantics/tck/typecheck.rs |  33 +++---
 4 files changed, 211 insertions(+), 211 deletions(-)
 create mode 100644 dhall/src/semantics/tck/tir.rs
 delete mode 100644 dhall/src/semantics/tck/tyexpr.rs

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

diff --git a/dhall/src/semantics/tck/mod.rs b/dhall/src/semantics/tck/mod.rs
index 1df2a48..93c8f48 100644
--- a/dhall/src/semantics/tck/mod.rs
+++ b/dhall/src/semantics/tck/mod.rs
@@ -1,6 +1,6 @@
 pub mod env;
-pub mod tyexpr;
+pub mod tir;
 pub mod typecheck;
 pub(crate) use env::*;
-pub(crate) use tyexpr::*;
+pub(crate) use tir::*;
 pub(crate) use typecheck::*;
diff --git a/dhall/src/semantics/tck/tir.rs b/dhall/src/semantics/tck/tir.rs
new file mode 100644
index 0000000..800d1b7
--- /dev/null
+++ b/dhall/src/semantics/tck/tir.rs
@@ -0,0 +1,193 @@
+use crate::error::{ErrorBuilder, TypeError};
+use crate::semantics::{mkerr, Hir, NzEnv, TyEnv, Value, ValueKind, VarEnv};
+use crate::syntax::{Builtin, Const, Span};
+use crate::{NormalizedExpr, ToExprOptions};
+
+/// The type of a type. 0 is `Type`, 1 is `Kind`, etc...
+#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Default)]
+pub(crate) struct Universe(u8);
+
+/// An expression representing a type
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub(crate) struct Type {
+    val: Value,
+    univ: Universe,
+}
+
+/// A hir expression plus its inferred type.
+/// Stands for "Typed intermediate representation"
+#[derive(Debug, Clone)]
+pub(crate) struct Tir {
+    hir: Hir,
+    ty: Type,
+}
+
+impl Universe {
+    pub fn from_const(c: Const) -> Self {
+        Universe(match c {
+            Const::Type => 0,
+            Const::Kind => 1,
+            Const::Sort => 2,
+        })
+    }
+    pub fn as_const(self) -> Option<Const> {
+        match self.0 {
+            0 => Some(Const::Type),
+            1 => Some(Const::Kind),
+            2 => Some(Const::Sort),
+            _ => None,
+        }
+    }
+    pub fn next(self) -> Self {
+        Universe(self.0 + 1)
+    }
+}
+
+impl Type {
+    pub fn new(val: Value, univ: Universe) -> Self {
+        Type { val, univ }
+    }
+    /// Creates a new Type and infers its universe by re-typechecking its value.
+    /// TODO: ideally avoid this function altogether. Would need to store types in RecordType and
+    /// PiClosure.
+    pub fn new_infer_universe(
+        env: &TyEnv,
+        val: Value,
+    ) -> Result<Self, TypeError> {
+        let c = val.to_hir(env.as_varenv()).typecheck(env)?.ty().as_const();
+        let u = match c {
+            Some(c) => c.to_universe(),
+            None => unreachable!(
+                "internal type error: this is not a type: {:?}",
+                val
+            ),
+        };
+        Ok(Type::new(val, u))
+    }
+    pub fn from_const(c: Const) -> Self {
+        Self::new(Value::from_const(c), c.to_universe().next())
+    }
+    pub fn from_builtin(b: Builtin) -> Self {
+        use Builtin::*;
+        match b {
+            Bool | Natural | Integer | Double | Text => {}
+            _ => unreachable!("this builtin is not a type: {}", b),
+        }
+
+        Self::new(Value::from_builtin(b), Universe::from_const(Const::Type))
+    }
+
+    /// Get the type of this type
+    pub fn ty(&self) -> Universe {
+        self.univ
+    }
+
+    pub fn to_value(&self) -> Value {
+        self.val.clone()
+    }
+    pub fn as_value(&self) -> &Value {
+        &self.val
+    }
+    pub fn into_value(self) -> Value {
+        self.val
+    }
+    pub fn as_const(&self) -> Option<Const> {
+        self.val.as_const()
+    }
+    pub fn kind(&self) -> &ValueKind {
+        self.val.kind()
+    }
+
+    pub fn to_hir(&self, venv: VarEnv) -> Hir {
+        self.val.to_hir(venv)
+    }
+    pub fn to_expr_tyenv(&self, tyenv: &TyEnv) -> NormalizedExpr {
+        self.val.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv)
+    }
+}
+
+impl Tir {
+    pub fn from_hir(hir: &Hir, ty: Type) -> Self {
+        Tir {
+            hir: hir.clone(),
+            ty,
+        }
+    }
+
+    pub fn span(&self) -> Span {
+        self.as_hir().span()
+    }
+    pub fn ty(&self) -> &Type {
+        &self.ty
+    }
+
+    pub fn to_hir(&self) -> Hir {
+        self.as_hir().clone()
+    }
+    pub fn as_hir(&self) -> &Hir {
+        &self.hir
+    }
+    /// Converts a closed expression back to the corresponding AST expression.
+    pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
+        self.as_hir().to_expr(opts)
+    }
+    pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
+        self.as_hir().to_expr_tyenv(env)
+    }
+
+    /// Eval the Tir. It will actually get evaluated only as needed on demand.
+    pub fn eval(&self, env: impl Into<NzEnv>) -> Value {
+        self.as_hir().eval(env.into())
+    }
+    pub fn ensure_is_type(&self, env: &TyEnv) -> Result<(), TypeError> {
+        if self.ty().as_const().is_none() {
+            return mkerr(
+                ErrorBuilder::new(format!(
+                    "Expected a type, found: `{}`",
+                    self.to_expr_tyenv(env),
+                ))
+                .span_err(
+                    self.span(),
+                    format!(
+                        "this has type: `{}`",
+                        self.ty().to_expr_tyenv(env)
+                    ),
+                )
+                .help(format!(
+                    "An expression in type position must have type `Type`, \
+                     `Kind` or `Sort`",
+                ))
+                .format(),
+            );
+        }
+        Ok(())
+    }
+    /// Evaluate to a Type.
+    pub fn eval_to_type(&self, env: &TyEnv) -> Result<Type, TypeError> {
+        self.ensure_is_type(env)?;
+        Ok(Type::new(
+            self.eval(env),
+            self.ty()
+                .as_const()
+                .expect("case handled in ensure_is_type")
+                .to_universe(),
+        ))
+    }
+    /// Eval a closed Tir (i.e. without free variables). It will actually get evaluated only as
+    /// needed on demand.
+    pub fn eval_closed_expr(&self) -> Value {
+        self.eval(NzEnv::new())
+    }
+    /// Eval a closed Tir fully and recursively;
+    pub fn rec_eval_closed_expr(&self) -> Value {
+        let val = self.eval_closed_expr();
+        val.normalize();
+        val
+    }
+}
+
+impl From<Const> for Universe {
+    fn from(x: Const) -> Universe {
+        Universe::from_const(x)
+    }
+}
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
deleted file mode 100644
index f6591ba..0000000
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ /dev/null
@@ -1,192 +0,0 @@
-use crate::error::{ErrorBuilder, TypeError};
-use crate::semantics::{mkerr, Hir, NzEnv, TyEnv, Value, ValueKind, VarEnv};
-use crate::syntax::{Builtin, Const, Span};
-use crate::{NormalizedExpr, ToExprOptions};
-
-/// The type of a type. 0 is `Type`, 1 is `Kind`, etc...
-#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Default)]
-pub(crate) struct Universe(u8);
-
-/// An expression representing a type
-#[derive(Debug, Clone, PartialEq, Eq)]
-pub(crate) struct Type {
-    val: Value,
-    univ: Universe,
-}
-
-/// A hir expression plus its inferred type.
-#[derive(Debug, Clone)]
-pub(crate) struct TyExpr {
-    hir: Hir,
-    ty: Type,
-}
-
-impl Universe {
-    pub fn from_const(c: Const) -> Self {
-        Universe(match c {
-            Const::Type => 0,
-            Const::Kind => 1,
-            Const::Sort => 2,
-        })
-    }
-    pub fn as_const(self) -> Option<Const> {
-        match self.0 {
-            0 => Some(Const::Type),
-            1 => Some(Const::Kind),
-            2 => Some(Const::Sort),
-            _ => None,
-        }
-    }
-    pub fn next(self) -> Self {
-        Universe(self.0 + 1)
-    }
-}
-
-impl Type {
-    pub fn new(val: Value, univ: Universe) -> Self {
-        Type { val, univ }
-    }
-    /// Creates a new Type and infers its universe by re-typechecking its value.
-    /// TODO: ideally avoid this function altogether. Would need to store types in RecordType and
-    /// PiClosure.
-    pub fn new_infer_universe(
-        env: &TyEnv,
-        val: Value,
-    ) -> Result<Self, TypeError> {
-        let c = val.to_hir(env.as_varenv()).typecheck(env)?.ty().as_const();
-        let u = match c {
-            Some(c) => c.to_universe(),
-            None => unreachable!(
-                "internal type error: this is not a type: {:?}",
-                val
-            ),
-        };
-        Ok(Type::new(val, u))
-    }
-    pub fn from_const(c: Const) -> Self {
-        Self::new(Value::from_const(c), c.to_universe().next())
-    }
-    pub fn from_builtin(b: Builtin) -> Self {
-        use Builtin::*;
-        match b {
-            Bool | Natural | Integer | Double | Text => {}
-            _ => unreachable!("this builtin is not a type: {}", b),
-        }
-
-        Self::new(Value::from_builtin(b), Universe::from_const(Const::Type))
-    }
-
-    /// Get the type of this type
-    pub fn ty(&self) -> Universe {
-        self.univ
-    }
-
-    pub fn to_value(&self) -> Value {
-        self.val.clone()
-    }
-    pub fn as_value(&self) -> &Value {
-        &self.val
-    }
-    pub fn into_value(self) -> Value {
-        self.val
-    }
-    pub fn as_const(&self) -> Option<Const> {
-        self.val.as_const()
-    }
-    pub fn kind(&self) -> &ValueKind {
-        self.val.kind()
-    }
-
-    pub fn to_hir(&self, venv: VarEnv) -> Hir {
-        self.val.to_hir(venv)
-    }
-    pub fn to_expr_tyenv(&self, tyenv: &TyEnv) -> NormalizedExpr {
-        self.val.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv)
-    }
-}
-
-impl TyExpr {
-    pub fn from_hir(hir: &Hir, ty: Type) -> Self {
-        TyExpr {
-            hir: hir.clone(),
-            ty,
-        }
-    }
-
-    pub fn span(&self) -> Span {
-        self.as_hir().span()
-    }
-    pub fn ty(&self) -> &Type {
-        &self.ty
-    }
-
-    pub fn to_hir(&self) -> Hir {
-        self.as_hir().clone()
-    }
-    pub fn as_hir(&self) -> &Hir {
-        &self.hir
-    }
-    /// Converts a closed expression back to the corresponding AST expression.
-    pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
-        self.as_hir().to_expr(opts)
-    }
-    pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
-        self.as_hir().to_expr_tyenv(env)
-    }
-
-    /// Eval the TyExpr. It will actually get evaluated only as needed on demand.
-    pub fn eval(&self, env: impl Into<NzEnv>) -> Value {
-        self.as_hir().eval(env.into())
-    }
-    pub fn ensure_is_type(&self, env: &TyEnv) -> Result<(), TypeError> {
-        if self.ty().as_const().is_none() {
-            return mkerr(
-                ErrorBuilder::new(format!(
-                    "Expected a type, found: `{}`",
-                    self.to_expr_tyenv(env),
-                ))
-                .span_err(
-                    self.span(),
-                    format!(
-                        "this has type: `{}`",
-                        self.ty().to_expr_tyenv(env)
-                    ),
-                )
-                .help(format!(
-                    "An expression in type position must have type `Type`, \
-                     `Kind` or `Sort`",
-                ))
-                .format(),
-            );
-        }
-        Ok(())
-    }
-    /// Evaluate to a Type.
-    pub fn eval_to_type(&self, env: &TyEnv) -> Result<Type, TypeError> {
-        self.ensure_is_type(env)?;
-        Ok(Type::new(
-            self.eval(env),
-            self.ty()
-                .as_const()
-                .expect("case handled in ensure_is_type")
-                .to_universe(),
-        ))
-    }
-    /// Eval a closed TyExpr (i.e. without free variables). It will actually get evaluated only as
-    /// needed on demand.
-    pub fn eval_closed_expr(&self) -> Value {
-        self.eval(NzEnv::new())
-    }
-    /// Eval a closed TyExpr fully and recursively;
-    pub fn rec_eval_closed_expr(&self) -> Value {
-        let val = self.eval_closed_expr();
-        val.normalize();
-        val
-    }
-}
-
-impl From<Const> for Universe {
-    fn from(x: Const) -> Universe {
-        Universe::from_const(x)
-    }
-}
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 45b3168..7bf15af 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -5,8 +5,8 @@ use std::collections::HashMap;
 use crate::error::{ErrorBuilder, TypeError, TypeMessage};
 use crate::semantics::merge_maps;
 use crate::semantics::{
-    type_of_builtin, Binder, BuiltinClosure, Closure, Hir, HirKind, TyEnv,
-    TyExpr, Type, Value, ValueKind,
+    type_of_builtin, Binder, BuiltinClosure, Closure, Hir, HirKind, Tir, TyEnv,
+    Type, Value, ValueKind,
 };
 use crate::syntax::{
     BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, LitKind, Span,
@@ -69,7 +69,7 @@ pub fn mk_span_err<T, S: ToString>(span: Span, msg: S) -> Result<T, TypeError> {
 /// layer.
 fn type_one_layer(
     env: &TyEnv,
-    ekind: ExprKind<TyExpr>,
+    ekind: ExprKind<Tir>,
     span: Span,
 ) -> Result<Type, TypeError> {
     let span_err = |msg: &str| mk_span_err(span.clone(), msg);
@@ -91,8 +91,7 @@ fn type_one_layer(
         ExprKind::Const(Const::Kind) => Type::from_const(Const::Sort),
         ExprKind::Builtin(b) => {
             let t_hir = type_of_builtin(*b);
-            let t_tyexpr = typecheck(&t_hir)?;
-            t_tyexpr.eval_to_type(env)?
+            typecheck(&t_hir)?.eval_to_type(env)?
         }
         ExprKind::Lit(LitKind::Bool(_)) => Type::from_builtin(Builtin::Bool),
         ExprKind::Lit(LitKind::Natural(_)) => {
@@ -712,9 +711,9 @@ pub(crate) fn type_with(
     env: &TyEnv,
     hir: &Hir,
     annot: Option<Type>,
-) -> Result<TyExpr, TypeError> {
-    let tyexpr = match hir.kind() {
-        HirKind::Var(var) => TyExpr::from_hir(hir, env.lookup(var)),
+) -> Result<Tir, TypeError> {
+    let tir = match hir.kind() {
+        HirKind::Var(var) => Tir::from_hir(hir, env.lookup(var)),
         HirKind::Expr(ExprKind::Var(_)) => {
             unreachable!("Hir should contain no unresolved variables")
         }
@@ -753,7 +752,7 @@ pub(crate) fn type_with(
             );
             let ty = Type::new(ty_hir.eval(env), u);
 
-            TyExpr::from_hir(hir, ty)
+            Tir::from_hir(hir, ty)
         }
         HirKind::Expr(ExprKind::Pi(binder, annot, body)) => {
             let annot = type_with(env, annot, None)?;
@@ -765,7 +764,7 @@ pub(crate) fn type_with(
             let ks = annot.ty().as_const().unwrap();
             let kt = body.ty().as_const().unwrap();
             let ty = Type::from_const(function_check(ks, kt));
-            TyExpr::from_hir(hir, ty)
+            Tir::from_hir(hir, ty)
         }
         HirKind::Expr(ExprKind::Let(binder, annot, val, body)) => {
             let val_annot = annot
@@ -777,39 +776,39 @@ pub(crate) fn type_with(
             let body_env = env.insert_value(&binder, val_nf, val.ty().clone());
             let body = type_with(&body_env, body, None)?;
             let ty = body.ty().clone();
-            TyExpr::from_hir(hir, ty)
+            Tir::from_hir(hir, ty)
         }
         HirKind::Expr(ekind) => {
             let ekind = ekind.traverse_ref(|e| type_with(env, e, None))?;
             let ty = type_one_layer(env, ekind, hir.span())?;
-            TyExpr::from_hir(hir, ty)
+            Tir::from_hir(hir, ty)
         }
     };
 
     if let Some(annot) = annot {
-        if *tyexpr.ty() != annot {
+        if *tir.ty() != annot {
             return mk_span_err(
                 hir.span(),
                 &format!(
                     "annot mismatch: {} != {}",
-                    tyexpr.ty().to_expr_tyenv(env),
+                    tir.ty().to_expr_tyenv(env),
                     annot.to_expr_tyenv(env)
                 ),
             );
         }
     }
 
-    Ok(tyexpr)
+    Ok(tir)
 }
 
 /// Typecheck an expression and return the expression annotated with types if type-checking
 /// succeeded, or an error if type-checking failed.
-pub(crate) fn typecheck(hir: &Hir) -> Result<TyExpr, TypeError> {
+pub(crate) fn typecheck(hir: &Hir) -> Result<Tir, TypeError> {
     type_with(&TyEnv::new(), hir, None)
 }
 
 /// Like `typecheck`, but additionally checks that the expression's type matches the provided type.
-pub(crate) fn typecheck_with(hir: &Hir, ty: Hir) -> Result<TyExpr, TypeError> {
+pub(crate) fn typecheck_with(hir: &Hir, ty: Hir) -> Result<Tir, TypeError> {
     let ty = typecheck(&ty)?.eval_to_type(&TyEnv::new())?;
     type_with(&TyEnv::new(), hir, Some(ty))
 }
-- 
cgit v1.2.3


From cd5e172002ce724be7bdd52883e121efa8817f20 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 17 Feb 2020 18:22:06 +0000
Subject: Rename Value to Nir

---
 dhall/src/semantics/tck/env.rs       |  4 +-
 dhall/src/semantics/tck/tir.rs       | 26 +++++------
 dhall/src/semantics/tck/typecheck.rs | 90 +++++++++++++++++-------------------
 3 files changed, 58 insertions(+), 62 deletions(-)

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

diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index f290c02..17b3cfe 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -1,4 +1,4 @@
-use crate::semantics::{AlphaVar, NameEnv, NzEnv, NzVar, Type, ValEnv, Value};
+use crate::semantics::{AlphaVar, NameEnv, Nir, NzEnv, NzVar, Type, ValEnv};
 use crate::syntax::Label;
 
 /// Environment for indexing variables.
@@ -61,7 +61,7 @@ impl TyEnv {
             items: self.items.insert_type(ty),
         }
     }
-    pub fn insert_value(&self, x: &Label, e: Value, ty: Type) -> Self {
+    pub fn insert_value(&self, x: &Label, e: Nir, ty: Type) -> Self {
         TyEnv {
             names: self.names.insert(x),
             items: self.items.insert_value(e, ty),
diff --git a/dhall/src/semantics/tck/tir.rs b/dhall/src/semantics/tck/tir.rs
index 800d1b7..908bf8f 100644
--- a/dhall/src/semantics/tck/tir.rs
+++ b/dhall/src/semantics/tck/tir.rs
@@ -1,5 +1,5 @@
 use crate::error::{ErrorBuilder, TypeError};
-use crate::semantics::{mkerr, Hir, NzEnv, TyEnv, Value, ValueKind, VarEnv};
+use crate::semantics::{mkerr, Hir, Nir, NirKind, NzEnv, TyEnv, VarEnv};
 use crate::syntax::{Builtin, Const, Span};
 use crate::{NormalizedExpr, ToExprOptions};
 
@@ -10,7 +10,7 @@ pub(crate) struct Universe(u8);
 /// An expression representing a type
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub(crate) struct Type {
-    val: Value,
+    val: Nir,
     univ: Universe,
 }
 
@@ -44,7 +44,7 @@ impl Universe {
 }
 
 impl Type {
-    pub fn new(val: Value, univ: Universe) -> Self {
+    pub fn new(val: Nir, univ: Universe) -> Self {
         Type { val, univ }
     }
     /// Creates a new Type and infers its universe by re-typechecking its value.
@@ -52,7 +52,7 @@ impl Type {
     /// PiClosure.
     pub fn new_infer_universe(
         env: &TyEnv,
-        val: Value,
+        val: Nir,
     ) -> Result<Self, TypeError> {
         let c = val.to_hir(env.as_varenv()).typecheck(env)?.ty().as_const();
         let u = match c {
@@ -65,7 +65,7 @@ impl Type {
         Ok(Type::new(val, u))
     }
     pub fn from_const(c: Const) -> Self {
-        Self::new(Value::from_const(c), c.to_universe().next())
+        Self::new(Nir::from_const(c), c.to_universe().next())
     }
     pub fn from_builtin(b: Builtin) -> Self {
         use Builtin::*;
@@ -74,7 +74,7 @@ impl Type {
             _ => unreachable!("this builtin is not a type: {}", b),
         }
 
-        Self::new(Value::from_builtin(b), Universe::from_const(Const::Type))
+        Self::new(Nir::from_builtin(b), Universe::from_const(Const::Type))
     }
 
     /// Get the type of this type
@@ -82,19 +82,19 @@ impl Type {
         self.univ
     }
 
-    pub fn to_value(&self) -> Value {
+    pub fn to_nir(&self) -> Nir {
         self.val.clone()
     }
-    pub fn as_value(&self) -> &Value {
+    pub fn as_nir(&self) -> &Nir {
         &self.val
     }
-    pub fn into_value(self) -> Value {
+    pub fn into_nir(self) -> Nir {
         self.val
     }
     pub fn as_const(&self) -> Option<Const> {
         self.val.as_const()
     }
-    pub fn kind(&self) -> &ValueKind {
+    pub fn kind(&self) -> &NirKind {
         self.val.kind()
     }
 
@@ -136,7 +136,7 @@ impl Tir {
     }
 
     /// Eval the Tir. It will actually get evaluated only as needed on demand.
-    pub fn eval(&self, env: impl Into<NzEnv>) -> Value {
+    pub fn eval(&self, env: impl Into<NzEnv>) -> Nir {
         self.as_hir().eval(env.into())
     }
     pub fn ensure_is_type(&self, env: &TyEnv) -> Result<(), TypeError> {
@@ -175,11 +175,11 @@ impl Tir {
     }
     /// Eval a closed Tir (i.e. without free variables). It will actually get evaluated only as
     /// needed on demand.
-    pub fn eval_closed_expr(&self) -> Value {
+    pub fn eval_closed_expr(&self) -> Nir {
         self.eval(NzEnv::new())
     }
     /// Eval a closed Tir fully and recursively;
-    pub fn rec_eval_closed_expr(&self) -> Value {
+    pub fn rec_eval_closed_expr(&self) -> Nir {
         let val = self.eval_closed_expr();
         val.normalize();
         val
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 7bf15af..42a9165 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -5,8 +5,8 @@ use std::collections::HashMap;
 use crate::error::{ErrorBuilder, TypeError, TypeMessage};
 use crate::semantics::merge_maps;
 use crate::semantics::{
-    type_of_builtin, Binder, BuiltinClosure, Closure, Hir, HirKind, Tir, TyEnv,
-    Type, Value, ValueKind,
+    type_of_builtin, Binder, BuiltinClosure, Closure, Hir, HirKind, Nir,
+    NirKind, Tir, TyEnv, Type,
 };
 use crate::syntax::{
     BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, LitKind, Span,
@@ -15,11 +15,11 @@ use crate::syntax::{
 fn check_rectymerge(
     span: &Span,
     env: &TyEnv,
-    x: Value,
-    y: Value,
+    x: Nir,
+    y: Nir,
 ) -> Result<(), TypeError> {
     let kts_x = match x.kind() {
-        ValueKind::RecordType(kts) => kts,
+        NirKind::RecordType(kts) => kts,
         _ => {
             return mk_span_err(
                 span.clone(),
@@ -28,7 +28,7 @@ fn check_rectymerge(
         }
     };
     let kts_y = match y.kind() {
-        ValueKind::RecordType(kts) => kts,
+        NirKind::RecordType(kts) => kts,
         _ => {
             return mk_span_err(
                 span.clone(),
@@ -118,7 +118,7 @@ fn type_one_layer(
         ExprKind::EmptyListLit(t) => {
             let t = t.eval_to_type(env)?;
             match t.kind() {
-                ValueKind::AppliedBuiltin(BuiltinClosure {
+                NirKind::AppliedBuiltin(BuiltinClosure {
                     b: Builtin::List,
                     args,
                     ..
@@ -139,18 +139,16 @@ fn type_one_layer(
                 return span_err("InvalidListType");
             }
 
-            let t = x.ty().to_value();
-            Value::from_builtin(Builtin::List)
-                .app(t)
-                .to_type(Const::Type)
+            let t = x.ty().to_nir();
+            Nir::from_builtin(Builtin::List).app(t).to_type(Const::Type)
         }
         ExprKind::SomeLit(x) => {
             if x.ty().ty().as_const() != Some(Const::Type) {
                 return span_err("InvalidOptionalType");
             }
 
-            let t = x.ty().to_value();
-            Value::from_builtin(Builtin::Optional)
+            let t = x.ty().to_nir();
+            Nir::from_builtin(Builtin::Optional)
                 .app(t)
                 .to_type(Const::Type)
         }
@@ -165,7 +163,7 @@ fn type_one_layer(
                     Entry::Occupied(_) => {
                         return span_err("RecordTypeDuplicateField")
                     }
-                    Entry::Vacant(e) => e.insert(v.ty().to_value()),
+                    Entry::Vacant(e) => e.insert(v.ty().to_nir()),
                 };
 
                 // Check that the fields have a valid kind
@@ -175,7 +173,7 @@ fn type_one_layer(
                 }
             }
 
-            Value::from_kind(ValueKind::RecordType(kts)).to_type(k)
+            Nir::from_kind(NirKind::RecordType(kts)).to_type(k)
         }
         ExprKind::RecordType(kts) => {
             use std::collections::hash_map::Entry;
@@ -230,21 +228,21 @@ fn type_one_layer(
         }
         ExprKind::Field(scrut, x) => {
             match scrut.ty().kind() {
-                ValueKind::RecordType(kts) => match kts.get(&x) {
+                NirKind::RecordType(kts) => match kts.get(&x) {
                     Some(val) => Type::new_infer_universe(env, val.clone())?,
                     None => return span_err("MissingRecordField"),
                 },
-                ValueKind::Const(_) => {
+                NirKind::Const(_) => {
                     let scrut = scrut.eval_to_type(env)?;
                     match scrut.kind() {
-                        ValueKind::UnionType(kts) => match kts.get(x) {
+                        NirKind::UnionType(kts) => match kts.get(x) {
                             // Constructor has type T -> < x: T, ... >
                             Some(Some(ty)) => {
-                                Value::from_kind(ValueKind::PiClosure {
+                                Nir::from_kind(NirKind::PiClosure {
                                     binder: Binder::new(x.clone()),
                                     annot: ty.clone(),
                                     closure: Closure::new_constant(
-                                        scrut.to_value(),
+                                        scrut.to_nir(),
                                     ),
                                 })
                                 .to_type(scrut.ty())
@@ -261,10 +259,8 @@ fn type_one_layer(
         ExprKind::Assert(t) => {
             let t = t.eval_to_type(env)?;
             match t.kind() {
-                ValueKind::Equivalence(x, y) if x == y => {}
-                ValueKind::Equivalence(..) => {
-                    return span_err("AssertMismatch")
-                }
+                NirKind::Equivalence(x, y) if x == y => {}
+                NirKind::Equivalence(..) => return span_err("AssertMismatch"),
                 _ => return span_err("AssertMustTakeEquivalence"),
             }
             t
@@ -272,8 +268,8 @@ fn type_one_layer(
         ExprKind::App(f, arg) => {
             match f.ty().kind() {
                 // TODO: store Type in closure
-                ValueKind::PiClosure { annot, closure, .. } => {
-                    if arg.ty().as_value() != annot {
+                NirKind::PiClosure { annot, closure, .. } => {
+                    if arg.ty().as_nir() != annot {
                         return mkerr(
                             ErrorBuilder::new(format!(
                                 "wrong type of function argument"
@@ -318,7 +314,7 @@ fn type_one_layer(
             }
         }
         ExprKind::BoolIf(x, y, z) => {
-            if *x.ty().kind() != ValueKind::from_builtin(Builtin::Bool) {
+            if *x.ty().kind() != NirKind::from_builtin(Builtin::Bool) {
                 return span_err("InvalidPredicate");
             }
             if y.ty().ty().as_const() != Some(Const::Type) {
@@ -336,12 +332,12 @@ fn type_one_layer(
 
             // Extract the LHS record type
             let kts_x = match x_type.kind() {
-                ValueKind::RecordType(kts) => kts,
+                NirKind::RecordType(kts) => kts,
                 _ => return span_err("MustCombineRecord"),
             };
             // Extract the RHS record type
             let kts_y = match y_type.kind() {
-                ValueKind::RecordType(kts) => kts,
+                NirKind::RecordType(kts) => kts,
                 _ => return span_err("MustCombineRecord"),
             };
 
@@ -352,10 +348,10 @@ fn type_one_layer(
             })?;
 
             let u = max(x.ty().ty(), y.ty().ty());
-            Value::from_kind(ValueKind::RecordType(kts)).to_type(u)
+            Nir::from_kind(NirKind::RecordType(kts)).to_type(u)
         }
         ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => {
-            check_rectymerge(&span, env, x.ty().to_value(), y.ty().to_value())?;
+            check_rectymerge(&span, env, x.ty().to_nir(), y.ty().to_nir())?;
 
             let hir = Hir::new(
                 HirKind::Expr(ExprKind::BinOp(
@@ -379,7 +375,7 @@ fn type_one_layer(
         }
         ExprKind::BinOp(BinOp::ListAppend, l, r) => {
             match l.ty().kind() {
-                ValueKind::AppliedBuiltin(BuiltinClosure {
+                NirKind::AppliedBuiltin(BuiltinClosure {
                     b: Builtin::List,
                     ..
                 }) => {}
@@ -431,14 +427,14 @@ fn type_one_layer(
         ExprKind::Merge(record, union, type_annot) => {
             let record_type = record.ty();
             let handlers = match record_type.kind() {
-                ValueKind::RecordType(kts) => kts,
+                NirKind::RecordType(kts) => kts,
                 _ => return span_err("Merge1ArgMustBeRecord"),
             };
 
             let union_type = union.ty();
             let variants = match union_type.kind() {
-                ValueKind::UnionType(kts) => Cow::Borrowed(kts),
-                ValueKind::AppliedBuiltin(BuiltinClosure {
+                NirKind::UnionType(kts) => Cow::Borrowed(kts),
+                NirKind::AppliedBuiltin(BuiltinClosure {
                     b: Builtin::Optional,
                     args,
                     ..
@@ -457,7 +453,7 @@ fn type_one_layer(
                 let handler_return_type: Type = match variants.get(x) {
                     // Union alternative with type
                     Some(Some(variant_type)) => match handler_type.kind() {
-                        ValueKind::PiClosure { closure, annot, .. } => {
+                        NirKind::PiClosure { closure, annot, .. } => {
                             if variant_type != annot {
                                 return mkerr(
                                     ErrorBuilder::new(format!(
@@ -578,7 +574,7 @@ fn type_one_layer(
             }
             let record_t = record.ty();
             let kts = match record_t.kind() {
-                ValueKind::RecordType(kts) => kts,
+                NirKind::RecordType(kts) => kts,
                 _ => {
                     return span_err("The argument to `toMap` must be a record")
                 }
@@ -598,7 +594,7 @@ fn type_one_layer(
                 let err_msg = "The type of `toMap x` must be of the form \
                                `List { mapKey : Text, mapValue : T }`";
                 let arg = match annot_val.kind() {
-                    ValueKind::AppliedBuiltin(BuiltinClosure {
+                    NirKind::AppliedBuiltin(BuiltinClosure {
                         b: Builtin::List,
                         args,
                         ..
@@ -606,14 +602,14 @@ fn type_one_layer(
                     _ => return span_err(err_msg),
                 };
                 let kts = match arg.kind() {
-                    ValueKind::RecordType(kts) => kts,
+                    NirKind::RecordType(kts) => kts,
                     _ => return span_err(err_msg),
                 };
                 if kts.len() != 2 {
                     return span_err(err_msg);
                 }
                 match kts.get(&"mapKey".into()) {
-                    Some(t) if *t == Value::from_builtin(Builtin::Text) => {}
+                    Some(t) if *t == Nir::from_builtin(Builtin::Text) => {}
                     _ => return span_err(err_msg),
                 }
                 match kts.get(&"mapValue".into()) {
@@ -632,10 +628,10 @@ fn type_one_layer(
                 }
 
                 let mut kts = HashMap::new();
-                kts.insert("mapKey".into(), Value::from_builtin(Builtin::Text));
+                kts.insert("mapKey".into(), Nir::from_builtin(Builtin::Text));
                 kts.insert("mapValue".into(), entry_type);
-                let output_type: Type = Value::from_builtin(Builtin::List)
-                    .app(Value::from_kind(ValueKind::RecordType(kts)))
+                let output_type: Type = Nir::from_builtin(Builtin::List)
+                    .app(Nir::from_kind(NirKind::RecordType(kts)))
                     .to_type(Const::Type);
                 if let Some(annot) = annot {
                     let annot_val = annot.eval_to_type(env)?;
@@ -649,7 +645,7 @@ fn type_one_layer(
         ExprKind::Projection(record, labels) => {
             let record_type = record.ty();
             let kts = match record_type.kind() {
-                ValueKind::RecordType(kts) => kts,
+                NirKind::RecordType(kts) => kts,
                 _ => return span_err("ProjectionMustBeRecord"),
             };
 
@@ -671,19 +667,19 @@ fn type_one_layer(
 
             Type::new_infer_universe(
                 env,
-                Value::from_kind(ValueKind::RecordType(new_kts)),
+                Nir::from_kind(NirKind::RecordType(new_kts)),
             )?
         }
         ExprKind::ProjectionByExpr(record, selection) => {
             let record_type = record.ty();
             let rec_kts = match record_type.kind() {
-                ValueKind::RecordType(kts) => kts,
+                NirKind::RecordType(kts) => kts,
                 _ => return span_err("ProjectionMustBeRecord"),
             };
 
             let selection_val = selection.eval_to_type(env)?;
             let sel_kts = match selection_val.kind() {
-                ValueKind::RecordType(kts) => kts,
+                NirKind::RecordType(kts) => kts,
                 _ => return span_err("ProjectionByExprTakesRecordType"),
             };
 
-- 
cgit v1.2.3


From ebe43bd6f1fd6feb1564ab9837399de7808b67b5 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 18 Feb 2020 18:39:10 +0000
Subject: Borrow relevant Hir from Tir

---
 dhall/src/semantics/tck/tir.rs       | 30 ++++++------------------------
 dhall/src/semantics/tck/typecheck.rs | 15 +++++++++------
 2 files changed, 15 insertions(+), 30 deletions(-)

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

diff --git a/dhall/src/semantics/tck/tir.rs b/dhall/src/semantics/tck/tir.rs
index 908bf8f..aeb7bf9 100644
--- a/dhall/src/semantics/tck/tir.rs
+++ b/dhall/src/semantics/tck/tir.rs
@@ -1,7 +1,7 @@
 use crate::error::{ErrorBuilder, TypeError};
 use crate::semantics::{mkerr, Hir, Nir, NirKind, NzEnv, TyEnv, VarEnv};
 use crate::syntax::{Builtin, Const, Span};
-use crate::{NormalizedExpr, ToExprOptions};
+use crate::NormalizedExpr;
 
 /// The type of a type. 0 is `Type`, 1 is `Kind`, etc...
 #[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Default)]
@@ -17,8 +17,8 @@ pub(crate) struct Type {
 /// A hir expression plus its inferred type.
 /// Stands for "Typed intermediate representation"
 #[derive(Debug, Clone)]
-pub(crate) struct Tir {
-    hir: Hir,
+pub(crate) struct Tir<'hir> {
+    hir: &'hir Hir,
     ty: Type,
 }
 
@@ -106,12 +106,9 @@ impl Type {
     }
 }
 
-impl Tir {
-    pub fn from_hir(hir: &Hir, ty: Type) -> Self {
-        Tir {
-            hir: hir.clone(),
-            ty,
-        }
+impl<'hir> Tir<'hir> {
+    pub fn from_hir(hir: &'hir Hir, ty: Type) -> Self {
+        Tir { hir, ty }
     }
 
     pub fn span(&self) -> Span {
@@ -127,10 +124,6 @@ impl Tir {
     pub fn as_hir(&self) -> &Hir {
         &self.hir
     }
-    /// Converts a closed expression back to the corresponding AST expression.
-    pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
-        self.as_hir().to_expr(opts)
-    }
     pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
         self.as_hir().to_expr_tyenv(env)
     }
@@ -173,17 +166,6 @@ impl Tir {
                 .to_universe(),
         ))
     }
-    /// Eval a closed Tir (i.e. without free variables). It will actually get evaluated only as
-    /// needed on demand.
-    pub fn eval_closed_expr(&self) -> Nir {
-        self.eval(NzEnv::new())
-    }
-    /// Eval a closed Tir fully and recursively;
-    pub fn rec_eval_closed_expr(&self) -> Nir {
-        let val = self.eval_closed_expr();
-        val.normalize();
-        val
-    }
 }
 
 impl From<Const> for Universe {
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 42a9165..0787b32 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -69,7 +69,7 @@ pub fn mk_span_err<T, S: ToString>(span: Span, msg: S) -> Result<T, TypeError> {
 /// layer.
 fn type_one_layer(
     env: &TyEnv,
-    ekind: ExprKind<Tir>,
+    ekind: ExprKind<Tir<'_>>,
     span: Span,
 ) -> Result<Type, TypeError> {
     let span_err = |msg: &str| mk_span_err(span.clone(), msg);
@@ -703,11 +703,11 @@ fn type_one_layer(
 
 /// `type_with` typechecks an expression in the provided environment. Optionally pass an annotation
 /// to compare with.
-pub(crate) fn type_with(
+pub(crate) fn type_with<'hir>(
     env: &TyEnv,
-    hir: &Hir,
+    hir: &'hir Hir,
     annot: Option<Type>,
-) -> Result<Tir, TypeError> {
+) -> Result<Tir<'hir>, TypeError> {
     let tir = match hir.kind() {
         HirKind::Var(var) => Tir::from_hir(hir, env.lookup(var)),
         HirKind::Expr(ExprKind::Var(_)) => {
@@ -799,12 +799,15 @@ pub(crate) fn type_with(
 
 /// Typecheck an expression and return the expression annotated with types if type-checking
 /// succeeded, or an error if type-checking failed.
-pub(crate) fn typecheck(hir: &Hir) -> Result<Tir, TypeError> {
+pub(crate) fn typecheck<'hir>(hir: &'hir Hir) -> Result<Tir<'hir>, TypeError> {
     type_with(&TyEnv::new(), hir, None)
 }
 
 /// Like `typecheck`, but additionally checks that the expression's type matches the provided type.
-pub(crate) fn typecheck_with(hir: &Hir, ty: Hir) -> Result<Tir, TypeError> {
+pub(crate) fn typecheck_with<'hir>(
+    hir: &'hir Hir,
+    ty: Hir,
+) -> Result<Tir<'hir>, TypeError> {
     let ty = typecheck(&ty)?.eval_to_type(&TyEnv::new())?;
     type_with(&TyEnv::new(), hir, Some(ty))
 }
-- 
cgit v1.2.3


From 7cbfc1a0d32766a383d1f48902502adaa2234d2f Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 18 Feb 2020 19:12:31 +0000
Subject: Avoid re-typechecking after import

---
 dhall/src/semantics/tck/typecheck.rs | 1 +
 1 file changed, 1 insertion(+)

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

diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 0787b32..972326b 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -710,6 +710,7 @@ pub(crate) fn type_with<'hir>(
 ) -> Result<Tir<'hir>, TypeError> {
     let tir = match hir.kind() {
         HirKind::Var(var) => Tir::from_hir(hir, env.lookup(var)),
+        HirKind::Import(_, ty) => Tir::from_hir(hir, ty.clone()),
         HirKind::Expr(ExprKind::Var(_)) => {
             unreachable!("Hir should contain no unresolved variables")
         }
-- 
cgit v1.2.3