Remove move type propagation through Value

5 files changed, 86 insertions, 237 deletions

diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
index d8eeb4a..48d4d96 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -24,7 +24,7 @@ use crate::semantics::resolve;
 use crate::semantics::resolve::ImportRoot;
 use crate::semantics::{typecheck, typecheck_with, TyExpr, Value, ValueKind};
 use crate::syntax::binary;
-use crate::syntax::{Builtin, Const, Expr};
+use crate::syntax::{Builtin, Expr};
 
 pub type ParsedExpr = Expr<Normalized>;
 pub type DecodedExpr = Expr<Normalized>;
@@ -148,18 +148,12 @@ impl Normalized {
         self.0
     }
 
-    pub(crate) fn from_const(c: Const) -> Self {
-        Normalized(Value::from_const(c))
-    }
-    pub(crate) fn from_kind_and_type(v: ValueKind, t: Normalized) -> Self {
-        Normalized(Value::from_kind_and_type(v, t.into_value()))
+    pub(crate) fn from_kind(v: ValueKind) -> Self {
+        Normalized(Value::from_kind(v))
     }
     pub(crate) fn from_value(th: Value) -> Self {
         Normalized(th)
     }
-    pub(crate) fn const_type() -> Self {
-        Normalized::from_const(Const::Type)
-    }
 
     pub fn make_builtin_type(b: Builtin) -> Self {
         Normalized::from_value(Value::from_builtin(b))
@@ -177,23 +171,17 @@ impl Normalized {
     pub fn make_record_type(
         kts: impl Iterator<Item = (String, Normalized)>,
     ) -> Self {
-        Normalized::from_kind_and_type(
-            ValueKind::RecordType(
-                kts.map(|(k, t)| (k.into(), t.into_value())).collect(),
-            ),
-            Normalized::const_type(),
-        )
+        Normalized::from_kind(ValueKind::RecordType(
+            kts.map(|(k, t)| (k.into(), t.into_value())).collect(),
+        ))
     }
     pub fn make_union_type(
         kts: impl Iterator<Item = (String, Option<Normalized>)>,
     ) -> Self {
-        Normalized::from_kind_and_type(
-            ValueKind::UnionType(
-                kts.map(|(k, t)| (k.into(), t.map(|t| t.into_value())))
-                    .collect(),
-            ),
-            Normalized::const_type(),
-        )
+        Normalized::from_kind(ValueKind::UnionType(
+            kts.map(|(k, t)| (k.into(), t.map(|t| t.into_value())))
+                .collect(),
+        ))
     }
 }
 
diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs
index 907d449..a513967 100644
--- a/dhall/src/semantics/builtins.rs
+++ b/dhall/src/semantics/builtins.rs
@@ -35,11 +35,11 @@ impl BuiltinClosure<Value> {
         }
     }
 
-    pub fn apply(&self, a: Value, f_ty: Value, ret_ty: &Value) -> ValueKind {
+    pub fn apply(&self, a: Value, f_ty: Value) -> ValueKind {
         use std::iter::once;
         let args = self.args.iter().cloned().chain(once(a.clone())).collect();
         let types = self.types.iter().cloned().chain(once(f_ty)).collect();
-        apply_builtin(self.b, args, ret_ty, types, self.env.clone())
+        apply_builtin(self.b, args, types, self.env.clone())
     }
     /// This doesn't break the invariant because we already checked that the appropriate arguments
     /// did not normalize to something that allows evaluation to proceed.
@@ -267,7 +267,6 @@ macro_rules! make_closure {
 fn apply_builtin(
     b: Builtin,
     args: Vec<Value>,
-    ty: &Value,
     types: Vec<Value>,
     env: NzEnv,
 ) -> ValueKind {
@@ -399,10 +398,7 @@ fn apply_builtin(
                     let mut kts = HashMap::new();
                     kts.insert("index".into(), Value::from_builtin(Natural));
                     kts.insert("value".into(), t.clone());
-                    let t = Value::from_kind_and_type(
-                        RecordType(kts),
-                        Value::from_const(Type),
-                    );
+                    let t = Value::from_kind(RecordType(kts));
 
                     // Construct the new list, with added indices
                     let list = match &*l_whnf {
@@ -414,18 +410,10 @@ fn apply_builtin(
                                     let mut kvs = HashMap::new();
                                     kvs.insert(
                                         "index".into(),
-                                        Value::from_kind_and_type(
-                                            NaturalLit(i),
-                                            Value::from_builtin(
-                                                Builtin::Natural,
-                                            ),
-                                        ),
+                                        Value::from_kind(NaturalLit(i)),
                                     );
                                     kvs.insert("value".into(), e.clone());
-                                    Value::from_kind_and_type(
-                                        RecordLit(kvs),
-                                        t.clone(),
-                                    )
+                                    Value::from_kind(RecordLit(kvs))
                                 })
                                 .collect(),
                         ),
@@ -449,7 +437,7 @@ fn apply_builtin(
                         ))
                         .app(t.clone()),
                     )
-                    .app(EmptyListLit(t.clone()).into_value_with_type(list_t)),
+                    .app(EmptyListLit(t.clone()).into_value()),
             )
         }
         (ListFold, [_, l, _, cons, nil]) => match &*l.kind() {
@@ -475,10 +463,7 @@ fn apply_builtin(
                         ))
                         .app(t.clone()),
                     )
-                    .app(
-                        EmptyOptionalLit(t.clone())
-                            .into_value_with_type(optional_t),
-                    ),
+                    .app(EmptyOptionalLit(t.clone()).into_value()),
             )
         }
         (OptionalFold, [_, v, _, just, nothing]) => match &*v.kind() {
@@ -492,20 +477,14 @@ fn apply_builtin(
                     λ(x : Natural) ->
                     1 + var(x)
                 )))
-                .app(
-                    NaturalLit(0)
-                        .into_value_with_type(Value::from_builtin(Natural)),
-                ),
+                .app(NaturalLit(0).into_value()),
         ),
 
         (NaturalFold, [n, t, succ, zero]) => match &*n.kind() {
             NaturalLit(0) => Ret::Value(zero.clone()),
             NaturalLit(n) => {
                 let fold = Value::from_builtin(NaturalFold)
-                    .app(
-                        NaturalLit(n - 1)
-                            .into_value_with_type(Value::from_builtin(Natural)),
-                    )
+                    .app(NaturalLit(n - 1).into_value())
                     .app(t.clone())
                     .app(succ.clone())
                     .app(zero.clone());
@@ -517,7 +496,7 @@ fn apply_builtin(
     };
     match ret {
         Ret::ValueKind(v) => v,
-        Ret::Value(v) => v.to_whnf_check_type(ty),
+        Ret::Value(v) => v.kind().clone(),
         Ret::DoneAsIs => AppliedBuiltin(BuiltinClosure {
             b,
             args,
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(),
         }
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()?;