Simplify type error type

5 files changed, 31 insertions, 56 deletions

diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs
index 844a3e4..5595c53 100644
--- a/dhall/src/error/mod.rs
+++ b/dhall/src/error/mod.rs
@@ -1,6 +1,5 @@
 use std::io::Error as IOError;
 
-use crate::semantics::core::context::TyCtx;
 use crate::semantics::core::value::Value;
 use crate::semantics::phase::resolve::ImportStack;
 use crate::semantics::phase::NormalizedExpr;
@@ -37,11 +36,10 @@ pub enum EncodeError {
     CBORError(serde_cbor::error::Error),
 }
 
-/// A structured type error that includes context
+/// A structured type error
 #[derive(Debug)]
 pub struct TypeError {
     message: TypeMessage,
-    context: TyCtx,
 }
 
 /// The specific type error
@@ -88,11 +86,8 @@ pub(crate) enum TypeMessage {
 }
 
 impl TypeError {
-    pub(crate) fn new(context: &TyCtx, message: TypeMessage) -> Self {
-        TypeError {
-            context: context.clone(),
-            message,
-        }
+    pub(crate) fn new(message: TypeMessage) -> Self {
+        TypeError { message }
     }
 }
 
@@ -100,7 +95,7 @@ impl std::fmt::Display for TypeError {
     fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
         use TypeMessage::*;
         let msg = match &self.message {
-            UnboundVariable(span) => span.error("Type error: Unbound variable"),
+            UnboundVariable(var) => var.error("Type error: Unbound variable"),
             InvalidInputType(v) => {
                 v.span().error("Type error: Invalid function input")
             }
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index f470019..dc6a116 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -3,7 +3,6 @@ use std::collections::HashMap;
 use std::rc::Rc;
 
 use crate::error::{TypeError, TypeMessage};
-use crate::semantics::core::context::TyCtx;
 use crate::semantics::core::var::{AlphaVar, Binder};
 use crate::semantics::phase::normalize::{apply_any, normalize_whnf};
 use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value};
@@ -438,7 +437,7 @@ impl ValueInternal {
     fn get_type(&self) -> Result<&Value, TypeError> {
         match &self.ty {
             Some(t) => Ok(t),
-            None => Err(TypeError::new(&TyCtx::new(), TypeMessage::Sort)),
+            None => Err(TypeError::new(TypeMessage::Sort)),
         }
     }
 
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index 15025c1..9e41f1e 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -14,27 +14,20 @@ use crate::syntax::{
 };
 
 fn tck_pi_type(
-    ctx: &TyCtx,
     binder: Binder,
     tx: Value,
     te: Value,
 ) -> Result<Value, TypeError> {
     use TypeMessage::*;
-    let ctx2 = ctx.insert_type(&binder, tx.clone());
 
     let ka = match tx.get_type()?.as_const() {
         Some(k) => k,
-        _ => return Err(TypeError::new(ctx, InvalidInputType(tx))),
+        _ => return Err(TypeError::new(InvalidInputType(tx))),
     };
 
     let kb = match te.get_type()?.as_const() {
         Some(k) => k,
-        _ => {
-            return Err(TypeError::new(
-                &ctx2,
-                InvalidOutputType(te.get_type()?),
-            ))
-        }
+        _ => return Err(TypeError::new(InvalidOutputType(te.get_type()?))),
     };
 
     let k = function_check(ka, kb);
@@ -46,7 +39,6 @@ fn tck_pi_type(
 }
 
 fn tck_record_type(
-    ctx: &TyCtx,
     kts: impl IntoIterator<Item = Result<(Label, Value), TypeError>>,
 ) -> Result<Value, TypeError> {
     use std::collections::hash_map::Entry;
@@ -59,13 +51,13 @@ fn tck_record_type(
         // Construct the union of the contained `Const`s
         match t.get_type()?.as_const() {
             Some(k2) => k = max(k, k2),
-            None => return Err(TypeError::new(ctx, InvalidFieldType(x, t))),
+            None => return Err(TypeError::new(InvalidFieldType(x, t))),
         }
         // Check for duplicated entries
         let entry = new_kts.entry(x);
         match &entry {
             Entry::Occupied(_) => {
-                return Err(TypeError::new(ctx, RecordTypeDuplicateField))
+                return Err(TypeError::new(RecordTypeDuplicateField))
             }
             Entry::Vacant(_) => entry.or_insert_with(|| t),
         };
@@ -77,7 +69,7 @@ fn tck_record_type(
     ))
 }
 
-fn tck_union_type<Iter>(ctx: &TyCtx, kts: Iter) -> Result<Value, TypeError>
+fn tck_union_type<Iter>(kts: Iter) -> Result<Value, TypeError>
 where
     Iter: IntoIterator<Item = Result<(Label, Option<Value>), TypeError>>,
 {
@@ -93,17 +85,14 @@ where
                 (None, Some(k2)) => k = Some(k2),
                 (Some(k1), Some(k2)) if k1 == k2 => {}
                 _ => {
-                    return Err(TypeError::new(
-                        ctx,
-                        InvalidFieldType(x, t.clone()),
-                    ))
+                    return Err(TypeError::new(InvalidFieldType(x, t.clone())))
                 }
             }
         }
         let entry = new_kts.entry(x);
         match &entry {
             Entry::Occupied(_) => {
-                return Err(TypeError::new(ctx, UnionTypeDuplicateField))
+                return Err(TypeError::new(UnionTypeDuplicateField))
             }
             Entry::Vacant(_) => entry.or_insert_with(|| t),
         };
@@ -313,7 +302,7 @@ fn type_with(ctx: &TyCtx, e: Expr<Normalized>) -> Result<Value, TypeError> {
             let body_type = body.get_type()?;
             Ok(Value::from_kind_and_type(
                 ValueKind::Lam(binder.clone(), annot.clone(), body),
-                tck_pi_type(ctx, binder, annot, body_type)?,
+                tck_pi_type(binder, annot, body_type)?,
             ))
         }
         Pi(x, ta, tb) => {
@@ -321,7 +310,7 @@ fn type_with(ctx: &TyCtx, e: Expr<Normalized>) -> Result<Value, TypeError> {
             let ta = type_with(ctx, ta.clone())?;
             let ctx2 = ctx.insert_type(&binder, ta.clone());
             let tb = type_with(&ctx2, tb.clone())?;
-            tck_pi_type(ctx, binder, ta, tb)
+            tck_pi_type(binder, ta, tb)
         }
         Let(x, t, v, e) => {
             let v = if let Some(t) = t {
@@ -337,9 +326,7 @@ fn type_with(ctx: &TyCtx, e: Expr<Normalized>) -> Result<Value, TypeError> {
         Embed(p) => Ok(p.clone().into_typed().into_value()),
         Var(var) => match ctx.lookup(&var) {
             Some(typed) => Ok(typed.clone()),
-            None => {
-                Err(TypeError::new(ctx, TypeMessage::UnboundVariable(span)))
-            }
+            None => Err(TypeError::new(TypeMessage::UnboundVariable(span))),
         },
         e => {
             // Typecheck recursively all subexpressions
@@ -364,7 +351,7 @@ fn type_last_layer(
     use syntax::Const::Type;
     use syntax::ExprKind::*;
     use TypeMessage::*;
-    let mkerr = |msg: TypeMessage| Err(TypeError::new(ctx, msg));
+    let mkerr = |msg: TypeMessage| Err(TypeError::new(msg));
 
     /// Intermediary return type
     enum Ret {
@@ -474,15 +461,12 @@ fn type_last_layer(
             RetTypeOnly(Value::from_builtin(syntax::Builtin::Optional).app(t))
         }
         RecordType(kts) => RetWhole(tck_record_type(
-            ctx,
             kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))),
         )?),
         UnionType(kts) => RetWhole(tck_union_type(
-            ctx,
             kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))),
         )?),
         RecordLit(kvs) => RetTypeOnly(tck_record_type(
-            ctx,
             kvs.iter().map(|(x, v)| Ok((x.clone(), v.get_type()?))),
         )?),
         Field(r, x) => {
@@ -502,7 +486,6 @@ fn type_last_layer(
                             Some(Some(t)) => {
                                 RetTypeOnly(
                                     tck_pi_type(
-                                        ctx,
                                         ctx.new_binder(x),
                                         t.clone(),
                                         r.under_binder(),
@@ -577,7 +560,6 @@ fn type_last_layer(
 
             // Construct the final record type from the union
             RetTypeOnly(tck_record_type(
-                ctx,
                 kts.into_iter().map(|(x, v)| Ok((x.clone(), v))),
             )?)
         }
@@ -627,7 +609,7 @@ fn type_last_layer(
                 },
             )?;
 
-            RetWhole(tck_record_type(ctx, kts.into_iter().map(Ok))?)
+            RetWhole(tck_record_type(kts.into_iter().map(Ok))?)
         }
         BinOp(o @ ListAppend, l, r) => {
             match &*l.get_type()?.as_whnf() {
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index 72f5b1d..983f3f8 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,6 +1,5 @@
 #![allow(dead_code)]
 use crate::error::{TypeError, TypeMessage};
-use crate::semantics::core::context::TyCtx;
 use crate::semantics::core::var::AlphaVar;
 use crate::semantics::phase::typecheck::rc;
 use crate::semantics::phase::Normalized;
@@ -40,7 +39,7 @@ impl TyExpr {
     pub fn get_type(&self) -> Result<Type, TypeError> {
         match &self.ty {
             Some(t) => Ok(t.clone()),
-            None => Err(TypeError::new(&TyCtx::new(), TypeMessage::Sort)),
+            None => Err(TypeError::new(TypeMessage::Sort)),
         }
     }
 
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index d86574a..7795d17 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -158,12 +158,12 @@ pub fn run_test(test: Test<'_>) -> Result<()> {
             parse_file_str(&file_path)?.resolve().unwrap_err();
         }
         TypeInferenceSuccess(expr_file_path, expected_file_path) => {
-            // let expr =
-            //     parse_file_str(&expr_file_path)?.resolve()?.typecheck()?;
-            // let ty = expr.get_type()?.to_expr();
-            let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr();
-            let tyexpr = crate::semantics::nze::nzexpr::typecheck(expr)?;
-            let ty = tyexpr.get_type()?.to_expr();
+            let expr =
+                parse_file_str(&expr_file_path)?.resolve()?.typecheck()?;
+            let ty = expr.get_type()?.to_expr();
+            // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr();
+            // let tyexpr = crate::semantics::nze::nzexpr::typecheck(expr)?;
+            // let ty = tyexpr.get_type()?.to_expr();
             let expected = parse_file_str(&expected_file_path)?.to_expr();
             assert_eq_display!(ty, expected);
         }
@@ -206,15 +206,15 @@ pub fn run_test(test: Test<'_>) -> Result<()> {
             }
         }
         Normalization(expr_file_path, expected_file_path) => {
-            // let expr = parse_file_str(&expr_file_path)?
-            //     .resolve()?
-            //     .typecheck()?
-            //     .normalize()
-            //     .to_expr();
-            let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr();
-            let expr = crate::semantics::nze::nzexpr::typecheck(expr)?
+            let expr = parse_file_str(&expr_file_path)?
+                .resolve()?
+                .typecheck()?
                 .normalize()
                 .to_expr();
+            // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr();
+            // let expr = crate::semantics::nze::nzexpr::typecheck(expr)?
+            //     .normalize()
+            //     .to_expr();
             let expected = parse_file_str(&expected_file_path)?.to_expr();
 
             assert_eq_display!(expr, expected);