Remove move type propagation through Value

2 files changed, 54 insertions, 154 deletions

diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index 3a981f4..c660fce 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -6,18 +6,16 @@ use crate::semantics::{
     Binder, BuiltinClosure, Closure, TextLit, TyExpr, TyExprKind, Value,
     ValueKind,
 };
-use crate::syntax::{
-    BinOp, Builtin, Const, ExprKind, InterpolatedTextContents,
-};
+use crate::syntax::{BinOp, Builtin, ExprKind, InterpolatedTextContents};
 use crate::Normalized;
 
-pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind {
+pub(crate) fn apply_any(f: Value, a: Value) -> ValueKind {
     match f.kind() {
         ValueKind::LamClosure { closure, .. } => {
-            closure.apply(a).to_whnf_check_type(ty)
+            closure.apply(a).kind().clone()
         }
         ValueKind::AppliedBuiltin(closure) => {
-            closure.apply(a, f.get_type_not_sort(), ty)
+            closure.apply(a, f.get_type_not_sort())
         }
         ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit(
             l.clone(),
@@ -102,12 +100,7 @@ enum Ret<'a> {
     Expr(ExprKind<Value, Normalized>),
 }
 
-fn apply_binop<'a>(
-    o: BinOp,
-    x: &'a Value,
-    y: &'a Value,
-    ty: &Value,
-) -> Option<Ret<'a>> {
+fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
     use BinOp::{
         BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus,
         NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge,
@@ -194,19 +187,12 @@ fn apply_binop<'a>(
             Ret::ValueRef(y)
         }
         (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
-            let kts = match ty.kind() {
-                RecordType(kts) => kts,
-                _ => unreachable!("Internal type error"),
-            };
-            let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |k, v1, v2| {
-                Ok(Value::from_partial_expr(
-                    ExprKind::BinOp(
-                        RecursiveRecordMerge,
-                        v1.clone(),
-                        v2.clone(),
-                    ),
-                    kts.get(k).expect("Internal type error").clone(),
-                ))
+            let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |_, v1, v2| {
+                Ok(Value::from_partial_expr(ExprKind::BinOp(
+                    RecursiveRecordMerge,
+                    v1.clone(),
+                    v2.clone(),
+                )))
             })?;
             Ret::ValueKind(RecordLit(kvs))
         }
@@ -217,14 +203,11 @@ fn apply_binop<'a>(
                 kts_y,
                 // If the Label exists for both records, then we hit the recursive case.
                 |_, l: &Value, r: &Value| {
-                    Ok(Value::from_partial_expr(
-                        ExprKind::BinOp(
-                            RecursiveRecordTypeMerge,
-                            l.clone(),
-                            r.clone(),
-                        ),
-                        ty.clone(),
-                    ))
+                    Ok(Value::from_partial_expr(ExprKind::BinOp(
+                        RecursiveRecordTypeMerge,
+                        l.clone(),
+                        r.clone(),
+                    )))
                 },
             )?;
             Ret::ValueKind(RecordType(kts))
@@ -240,7 +223,6 @@ fn apply_binop<'a>(
 
 pub(crate) fn normalize_one_layer(
     expr: ExprKind<Value, Normalized>,
-    ty: &Value,
     env: &NzEnv,
 ) -> ValueKind {
     use ValueKind::{
@@ -318,7 +300,7 @@ pub(crate) fn normalize_one_layer(
                 }
             }
         }
-        ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y, ty) {
+        ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y) {
             Some(ret) => ret,
             None => Ret::Expr(expr),
         },
@@ -335,7 +317,6 @@ pub(crate) fn normalize_one_layer(
             PartialExpr(ExprKind::Projection(v2, _)) => {
                 return normalize_one_layer(
                     ExprKind::Projection(v2.clone(), ls.clone()),
-                    ty,
                     env,
                 )
             }
@@ -361,45 +342,26 @@ pub(crate) fn normalize_one_layer(
                     None => {
                         return normalize_one_layer(
                             ExprKind::Field(x.clone(), l.clone()),
-                            ty,
                             env,
                         )
                     }
                 },
                 (RecordLit(kvs), _) => match kvs.get(l) {
                     Some(r) => Ret::Expr(ExprKind::Field(
-                        Value::from_kind_and_type(
-                            PartialExpr(ExprKind::BinOp(
-                                BinOp::RightBiasedRecordMerge,
-                                Value::from_kind_and_type(
-                                    RecordLit({
-                                        let mut kvs = HashMap::new();
-                                        kvs.insert(l.clone(), r.clone());
-                                        kvs
-                                    }),
-                                    Value::from_kind_and_type(
-                                        RecordType({
-                                            let mut kvs = HashMap::new();
-                                            kvs.insert(
-                                                l.clone(),
-                                                r.get_type_not_sort(),
-                                            );
-                                            kvs
-                                        }),
-                                        r.get_type_not_sort()
-                                            .get_type_not_sort(),
-                                    ),
-                                ),
-                                y.clone(),
-                            )),
-                            v.get_type_not_sort(),
-                        ),
+                        Value::from_kind(PartialExpr(ExprKind::BinOp(
+                            BinOp::RightBiasedRecordMerge,
+                            Value::from_kind(RecordLit({
+                                let mut kvs = HashMap::new();
+                                kvs.insert(l.clone(), r.clone());
+                                kvs
+                            })),
+                            y.clone(),
+                        ))),
                         l.clone(),
                     )),
                     None => {
                         return normalize_one_layer(
                             ExprKind::Field(y.clone(), l.clone()),
-                            ty,
                             env,
                         )
                     }
@@ -416,7 +378,6 @@ pub(crate) fn normalize_one_layer(
                     None => {
                         return normalize_one_layer(
                             ExprKind::Field(y.clone(), l.clone()),
-                            ty,
                             env,
                         )
                     }
@@ -426,7 +387,6 @@ pub(crate) fn normalize_one_layer(
                     None => {
                         return normalize_one_layer(
                             ExprKind::Field(x.clone(), l.clone()),
-                            ty,
                             env,
                         )
                     }
@@ -482,22 +442,9 @@ pub(crate) fn normalize_one_layer(
                     .sorted_by_key(|(k, _)| k.clone())
                     .map(|(k, v)| {
                         let mut rec = HashMap::new();
-                        let mut rec_ty = HashMap::new();
                         rec.insert("mapKey".into(), Value::from_text(k));
                         rec.insert("mapValue".into(), v.clone());
-                        rec_ty.insert(
-                            "mapKey".into(),
-                            Value::from_builtin(Builtin::Text),
-                        );
-                        rec_ty.insert("mapValue".into(), v.get_type_not_sort());
-
-                        Value::from_kind_and_type(
-                            ValueKind::RecordLit(rec),
-                            Value::from_kind_and_type(
-                                ValueKind::RecordType(rec_ty),
-                                Value::from_const(Const::Type),
-                            ),
-                        )
+                        Value::from_kind(ValueKind::RecordLit(rec))
                     })
                     .collect(),
             )),
@@ -507,8 +454,8 @@ pub(crate) fn normalize_one_layer(
 
     match ret {
         Ret::ValueKind(v) => v,
-        Ret::Value(v) => v.to_whnf_check_type(ty),
-        Ret::ValueRef(v) => v.to_whnf_check_type(ty),
+        Ret::Value(v) => v.kind().clone(),
+        Ret::ValueRef(v) => v.kind().clone(),
         Ret::Expr(expr) => ValueKind::PartialExpr(expr),
     }
 }
@@ -521,17 +468,16 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind {
             let annot = annot.eval(env);
             ValueKind::LamClosure {
                 binder: Binder::new(binder.clone()),
-                annot: annot.clone(),
-                closure: Closure::new(annot, env, body.clone()),
+                annot: annot,
+                closure: Closure::new(env, body.clone()),
             }
         }
         TyExprKind::Expr(ExprKind::Pi(binder, annot, body)) => {
             let annot = annot.eval(env);
-            let closure = Closure::new(annot.clone(), env, body.clone());
             ValueKind::PiClosure {
                 binder: Binder::new(binder.clone()),
                 annot,
-                closure,
+                closure: Closure::new(env, body.clone()),
             }
         }
         TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => {
@@ -539,12 +485,8 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind {
             body.eval(&env.insert_value_noty(val)).kind().clone()
         }
         TyExprKind::Expr(e) => {
-            let ty = match tye.get_type() {
-                Ok(ty) => ty,
-                Err(_) => return ValueKind::Const(Const::Sort),
-            };
             let e = e.map_ref(|tye| tye.eval(env));
-            normalize_one_layer(e, &ty, env)
+            normalize_one_layer(e, env)
         }
     }
 }
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index 203b479..47c50a4 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -5,8 +5,8 @@ use crate::error::{TypeError, TypeMessage};
 use crate::semantics::nze::lazy;
 use crate::semantics::{
     apply_any, normalize_one_layer, normalize_tyexpr_whnf, squash_textlit,
-    type_of_builtin, type_with, typecheck, Binder, BuiltinClosure, NzEnv,
-    NzVar, TyEnv, TyExpr, TyExprKind, VarEnv,
+    type_with, Binder, BuiltinClosure, NzEnv, NzVar, TyEnv, TyExpr, TyExprKind,
+    VarEnv,
 };
 use crate::syntax::{
     BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label,
@@ -39,7 +39,6 @@ pub(crate) enum Thunk {
     PartialExpr {
         env: NzEnv,
         expr: ExprKind<Value, Normalized>,
-        ty: Value,
     },
 }
 
@@ -47,11 +46,7 @@ pub(crate) enum Thunk {
 #[derive(Debug, Clone)]
 pub(crate) enum Closure {
     /// Normal closure
-    Closure {
-        arg_ty: Value,
-        env: NzEnv,
-        body: TyExpr,
-    },
+    Closure { env: NzEnv, body: TyExpr },
     /// Closure that ignores the argument passed
     ConstantClosure { body: Value },
 }
@@ -130,21 +125,18 @@ impl Value {
         .into_value()
     }
     /// Construct a Value from a partially normalized expression that's not in WHNF.
-    pub(crate) fn from_partial_expr(
-        e: ExprKind<Value, Normalized>,
-        ty: Value,
-    ) -> Value {
+    pub(crate) fn from_partial_expr(e: ExprKind<Value, Normalized>) -> Value {
         // TODO: env
         let env = NzEnv::new();
         ValueInternal::from_thunk(
-            Thunk::from_partial_expr(env, e, ty.clone()),
+            Thunk::from_partial_expr(env, e),
             Some(Value::const_kind()),
             Span::Artificial,
         )
         .into_value()
     }
     /// Make a Value from a ValueKind
-    pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value {
+    pub(crate) fn from_kind(v: ValueKind) -> Value {
         ValueInternal::from_whnf(v, Some(Value::const_kind()), Span::Artificial)
             .into_value()
     }
@@ -170,16 +162,12 @@ impl Value {
         Self::from_builtin_env(b, &NzEnv::new())
     }
     pub(crate) fn from_builtin_env(b: Builtin, env: &NzEnv) -> Self {
-        Value::from_kind_and_type(
-            ValueKind::from_builtin_env(b, env.clone()),
-            typecheck(&type_of_builtin(b)).unwrap().eval_closed_expr(),
-        )
+        Value::from_kind(ValueKind::from_builtin_env(b, env.clone()))
     }
     pub(crate) fn from_text(txt: impl ToString) -> Self {
-        Value::from_kind_and_type(
-            ValueKind::TextLit(TextLit::from_text(txt.to_string())),
-            Value::from_builtin(Builtin::Text),
-        )
+        Value::from_kind(ValueKind::TextLit(TextLit::from_text(
+            txt.to_string(),
+        )))
     }
 
     pub(crate) fn as_const(&self) -> Option<Const> {
@@ -210,14 +198,6 @@ impl Value {
     pub(crate) fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
         self.to_tyexpr(env.as_varenv()).to_expr_tyenv(env)
     }
-    pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind {
-        self.kind().clone()
-    }
-    /// Before discarding type information, check that it matches the expected return type.
-    pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueKind {
-        self.check_type(ty);
-        self.to_whnf_ignore_type()
-    }
 
     /// Normalizes contents to normal form; faster than `normalize` if
     /// no one else shares this.
@@ -234,33 +214,19 @@ impl Value {
     }
 
     pub(crate) fn app(&self, v: Value) -> Value {
-        Value::from_kind_and_type(
-            apply_any(self.clone(), v, &Value::const_kind()),
-            Value::const_kind(),
-        )
+        Value::from_kind(apply_any(self.clone(), v))
     }
 
-    /// In debug mode, panic if the provided type doesn't match the value's type.
-    /// Otherwise does nothing.
-    pub(crate) fn check_type(&self, _ty: &Value) {
-        // TODO: reenable
-        // debug_assert_eq!(
-        //     Some(ty),
-        //     self.get_type().ok().as_ref(),
-        //     "Internal type error"
-        // );
-    }
     pub(crate) fn get_type(&self, tyenv: &TyEnv) -> Result<Value, TypeError> {
         let expr = self.to_tyexpr(tyenv.as_varenv()).to_expr_tyenv(tyenv);
         type_with(tyenv, &expr).unwrap().get_type()
     }
-    pub(crate) fn get_type_noenv(&self) -> Result<Value, TypeError> {
-        Ok(self.0.get_type()?.clone())
-    }
     /// When we know the value isn't `Sort`, this gets the type directly
     pub(crate) fn get_type_not_sort(&self) -> Value {
-        self.get_type_noenv()
+        self.0
+            .get_type()
             .expect("Internal type error: value is `Sort` but shouldn't be")
+            .clone()
     }
 
     pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr {
@@ -422,8 +388,8 @@ impl ValueInternal {
 }
 
 impl ValueKind {
-    pub(crate) fn into_value_with_type(self, t: Value) -> Value {
-        Value::from_kind_and_type(self, t)
+    pub(crate) fn into_value(self) -> Value {
+        Value::from_kind(self)
     }
 
     pub(crate) fn normalize(&self) {
@@ -504,24 +470,20 @@ impl Thunk {
     pub fn from_partial_expr(
         env: NzEnv,
         expr: ExprKind<Value, Normalized>,
-        ty: Value,
     ) -> Self {
-        Thunk::PartialExpr { env, expr, ty }
+        Thunk::PartialExpr { env, expr }
     }
     pub fn eval(self) -> ValueKind {
         match self {
             Thunk::Thunk { env, body } => normalize_tyexpr_whnf(&body, &env),
-            Thunk::PartialExpr { env, expr, ty } => {
-                normalize_one_layer(expr, &ty, &env)
-            }
+            Thunk::PartialExpr { env, expr } => normalize_one_layer(expr, &env),
         }
     }
 }
 
 impl Closure {
-    pub fn new(arg_ty: Value, env: &NzEnv, body: TyExpr) -> Self {
+    pub fn new(env: &NzEnv, body: TyExpr) -> Self {
         Closure::Closure {
-            arg_ty,
             env: env.clone(),
             body,
         }
@@ -541,12 +503,8 @@ impl Closure {
     }
     fn apply_var(&self, var: NzVar) -> Value {
         match self {
-            Closure::Closure { arg_ty, .. } => {
-                let val = Value::from_kind_and_type(
-                    ValueKind::Var(var),
-                    arg_ty.clone(),
-                );
-                self.apply(val)
+            Closure::Closure { .. } => {
+                self.apply(Value::from_kind(ValueKind::Var(var)))
             }
             Closure::ConstantClosure { body, .. } => body.clone(),
         }