Revert "Make SubExpr generic in the variable labels type"

This reverts commit 4c159640e5ee77ffa48b85a5bffa56350cf933ef.

6 files changed, 83 insertions, 100 deletions

diff --git a/dhall/src/binary.rs b/dhall/src/binary.rs
index 0d9f28a..9c31d4c 100644
--- a/dhall/src/binary.rs
+++ b/dhall/src/binary.rs
@@ -2,7 +2,7 @@ use dhall_syntax::*;
 use itertools::*;
 use serde_cbor::value::value as cbor;
 
-type ParsedExpr = SubExpr<Label, X, Import>;
+type ParsedExpr = SubExpr<X, Import>;
 
 #[derive(Debug)]
 pub enum DecodeError {
@@ -18,32 +18,28 @@ pub fn decode(data: &[u8]) -> Result<ParsedExpr, DecodeError> {
 }
 
 fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> {
-    use cbor::Value::{Array, Bool, Null, Object, String, F64, I64, U64};
+    use cbor::Value::*;
     use dhall_syntax::{BinOp, Builtin, Const};
-    use ExprF::{
-        Annot, App, BoolIf, BoolLit, DoubleLit, Embed, EmptyListLit, Field,
-        IntegerLit, Lam, Let, Merge, NEListLit, NaturalLit, OldOptionalLit, Pi,
-        RecordLit, RecordType, SomeLit, TextLit, UnionLit, UnionType,
-    };
+    use ExprF::*;
     Ok(rc(match data {
         String(s) => match Builtin::parse(s) {
             Some(b) => ExprF::Builtin(b),
             None => match s.as_str() {
                 "True" => BoolLit(true),
                 "False" => BoolLit(false),
-                "Type" => ExprF::Const(Const::Type),
-                "Kind" => ExprF::Const(Const::Kind),
-                "Sort" => ExprF::Const(Const::Sort),
+                "Type" => Const(Const::Type),
+                "Kind" => Const(Const::Kind),
+                "Sort" => Const(Const::Sort),
                 _ => Err(DecodeError::WrongFormatError("builtin".to_owned()))?,
             },
         },
-        U64(n) => ExprF::Var(Var(Label::from("_"), *n as usize)),
+        U64(n) => Var(V(Label::from("_"), *n as usize)),
         F64(x) => DoubleLit((*x).into()),
         Bool(b) => BoolLit(*b),
         Array(vec) => match vec.as_slice() {
             [String(l), U64(n)] => {
                 let l = Label::from(l.as_str());
-                ExprF::Var(Var(l, *n as usize))
+                Var(V(l, *n as usize))
             }
             [U64(0), f, args..] => {
                 let mut f = cbor_value_to_dhall(&f)?;
@@ -96,7 +92,7 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> {
                         Err(DecodeError::WrongFormatError("binop".to_owned()))?
                     }
                 };
-                ExprF::BinOp(op, x, y)
+                BinOp(op, x, y)
             }
             [U64(4), t] => {
                 let t = cbor_value_to_dhall(&t)?;
diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index efc3928..5bde68f 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -23,17 +23,15 @@ macro_rules! derive_other_traits {
     };
 }
 
-type OutputSubExpr = SubExpr<Label, X, X>;
-
 #[derive(Debug, Clone)]
 pub(crate) struct Parsed(
-    pub(crate) SubExpr<Label, Span, Import>,
+    pub(crate) SubExpr<Span, Import>,
     pub(crate) ImportRoot,
 );
 derive_other_traits!(Parsed);
 
 #[derive(Debug, Clone)]
-pub(crate) struct Resolved(pub(crate) SubExpr<Label, Span, Normalized>);
+pub(crate) struct Resolved(pub(crate) SubExpr<Span, Normalized>);
 derive_other_traits!(Resolved);
 
 pub(crate) use self::typed::TypedInternal;
@@ -59,12 +57,12 @@ impl std::fmt::Display for Normalized {
 }
 
 mod typed {
-    use super::{OutputSubExpr, Type, Typed};
+    use super::{Type, Typed};
     use crate::normalize::{Thunk, Value};
     use crate::typecheck::{
         TypeError, TypeInternal, TypeMessage, TypecheckContext,
     };
-    use dhall_syntax::{Const, Label, Var};
+    use dhall_syntax::{Const, Label, SubExpr, V, X};
     use std::borrow::Cow;
 
     #[derive(Debug, Clone)]
@@ -92,7 +90,7 @@ mod typed {
             }
         }
 
-        pub(crate) fn to_expr(&self) -> OutputSubExpr {
+        pub(crate) fn to_expr(&self) -> SubExpr<X, X> {
             self.to_value().normalize_to_expr()
         }
 
@@ -131,7 +129,7 @@ mod typed {
             }
         }
 
-        pub(crate) fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+        pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
             match self {
                 TypedInternal::Value(th, t) => TypedInternal::Value(
                     th.shift(delta, var),
@@ -141,11 +139,7 @@ mod typed {
             }
         }
 
-        pub(crate) fn subst_shift(
-            &self,
-            var: &Var<Label>,
-            val: &Typed,
-        ) -> Self {
+        pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
             match self {
                 TypedInternal::Value(th, t) => TypedInternal::Value(
                     th.subst_shift(var, val),
@@ -164,7 +158,7 @@ mod typed {
 ///
 /// For a more general notion of "type", see [Type].
 #[derive(Debug, Clone)]
-pub struct SimpleType(pub(crate) OutputSubExpr);
+pub struct SimpleType(pub(crate) SubExpr<X, X>);
 derive_other_traits!(SimpleType);
 
 pub(crate) use crate::typecheck::TypeInternal;
@@ -184,16 +178,16 @@ impl std::fmt::Display for Type {
 
 // Exposed for the macros
 #[doc(hidden)]
-impl From<SimpleType> for OutputSubExpr {
-    fn from(x: SimpleType) -> OutputSubExpr {
+impl From<SimpleType> for SubExpr<X, X> {
+    fn from(x: SimpleType) -> SubExpr<X, X> {
         x.0
     }
 }
 
 // Exposed for the macros
 #[doc(hidden)]
-impl From<OutputSubExpr> for SimpleType {
-    fn from(x: OutputSubExpr) -> SimpleType {
+impl From<SubExpr<X, X>> for SimpleType {
+    fn from(x: SubExpr<X, X>) -> SimpleType {
         SimpleType(x)
     }
 }
@@ -210,7 +204,7 @@ impl Normalized {
     pub(crate) fn from_thunk_and_type(th: Thunk, t: Type) -> Self {
         Normalized(TypedInternal::from_thunk_and_type(th, t))
     }
-    pub(crate) fn to_expr(&self) -> OutputSubExpr {
+    pub(crate) fn to_expr(&self) -> SubExpr<X, X> {
         self.0.to_expr()
     }
     pub(crate) fn to_value(&self) -> Value {
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 3de12ee..8ae746d 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -6,13 +6,13 @@ use dhall_proc_macros as dhall;
 use dhall_syntax::context::Context;
 use dhall_syntax::{
     rc, BinOp, Builtin, Const, ExprF, Integer, InterpolatedText,
-    InterpolatedTextContents, Label, Natural, Span, SubExpr, Var, X,
+    InterpolatedTextContents, Label, Natural, Span, SubExpr, V, X,
 };
 
 use crate::expr::{Normalized, Type, Typed, TypedInternal};
 
-type InputSubExpr = SubExpr<Label, Span, Normalized>;
-type OutputSubExpr = SubExpr<Label, X, X>;
+type InputSubExpr = SubExpr<Span, Normalized>;
+type OutputSubExpr = SubExpr<X, X>;
 
 impl Typed {
     /// Reduce an expression to its normal form, performing beta reduction
@@ -38,11 +38,11 @@ impl Typed {
         Normalized(internal)
     }
 
-    pub(crate) fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+    pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         Typed(self.0.shift(delta, var))
     }
 
-    pub(crate) fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
+    pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
         Typed(self.0.subst_shift(var, val))
     }
 
@@ -58,11 +58,11 @@ impl Typed {
 #[derive(Debug, Clone)]
 enum EnvItem {
     Thunk(Thunk),
-    Skip(Var<Label>),
+    Skip(V<Label>),
 }
 
 impl EnvItem {
-    fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         use EnvItem::*;
         match self {
             Thunk(e) => Thunk(e.shift(delta, var)),
@@ -70,7 +70,7 @@ impl EnvItem {
         }
     }
 
-    pub(crate) fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
+    pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
         match self {
             EnvItem::Thunk(e) => EnvItem::Thunk(e.subst_shift(var, val)),
             EnvItem::Skip(v) if v == var => EnvItem::Thunk(val.to_thunk()),
@@ -93,8 +93,8 @@ impl NormalizationContext {
                 .insert(x.clone(), EnvItem::Skip(x.into())),
         ))
     }
-    fn lookup(&self, var: &Var<Label>) -> Value {
-        let Var(x, n) = var;
+    fn lookup(&self, var: &V<Label>) -> Value {
+        let V(x, n) = var;
         match self.0.lookup(x, *n) {
             Some(EnvItem::Thunk(t)) => t.to_value(),
             Some(EnvItem::Skip(newvar)) => Value::Var(newvar.clone()),
@@ -118,11 +118,11 @@ impl NormalizationContext {
         NormalizationContext(Rc::new(ctx))
     }
 
-    fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         NormalizationContext(Rc::new(self.0.map(|_, e| e.shift(delta, var))))
     }
 
-    fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
+    fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
         NormalizationContext(Rc::new(
             self.0.map(|_, e| e.subst_shift(var, val)),
         ))
@@ -144,7 +144,7 @@ pub(crate) enum Value {
     NaturalSuccClosure,
     Pi(Label, TypeThunk, TypeThunk),
 
-    Var(Var<Label>),
+    Var(V<Label>),
     Const(Const),
     BoolLit(bool),
     NaturalLit(Natural),
@@ -403,7 +403,7 @@ impl Value {
         Value::AppliedBuiltin(b, vec![])
     }
 
-    fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         match self {
             Value::Lam(x, t, e) => Value::Lam(
                 x.clone(),
@@ -500,7 +500,7 @@ impl Value {
         }
     }
 
-    pub(crate) fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
+    pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
         match self {
             Value::Lam(x, t, e) => Value::Lam(
                 x.clone(),
@@ -616,7 +616,7 @@ mod thunk {
         OutputSubExpr, Value,
     };
     use crate::expr::Typed;
-    use dhall_syntax::{Label, Var};
+    use dhall_syntax::{Label, V};
     use std::cell::{Ref, RefCell};
     use std::rc::Rc;
 
@@ -693,7 +693,7 @@ mod thunk {
             }
         }
 
-        fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+        fn shift(&self, delta: isize, var: &V<Label>) -> Self {
             match self {
                 ThunkInternal::Unnormalized(ctx, e) => {
                     ThunkInternal::Unnormalized(
@@ -707,7 +707,7 @@ mod thunk {
             }
         }
 
-        fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
+        fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
             match self {
                 ThunkInternal::Unnormalized(ctx, e) => {
                     ThunkInternal::Unnormalized(
@@ -805,15 +805,11 @@ mod thunk {
             apply_any(self.clone(), th)
         }
 
-        pub(crate) fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+        pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
             self.0.borrow().shift(delta, var).into_thunk()
         }
 
-        pub(crate) fn subst_shift(
-            &self,
-            var: &Var<Label>,
-            val: &Typed,
-        ) -> Self {
+        pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
             self.0.borrow().subst_shift(var, val).into_thunk()
         }
     }
@@ -859,14 +855,14 @@ impl TypeThunk {
         self.normalize_nf().normalize_to_expr()
     }
 
-    fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         match self {
             TypeThunk::Thunk(th) => TypeThunk::Thunk(th.shift(delta, var)),
             TypeThunk::Type(t) => TypeThunk::Type(t.shift(delta, var)),
         }
     }
 
-    pub(crate) fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
+    pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
         match self {
             TypeThunk::Thunk(th) => TypeThunk::Thunk(th.subst_shift(var, val)),
             TypeThunk::Type(t) => TypeThunk::Type(t.subst_shift(var, val)),
diff --git a/dhall/src/serde.rs b/dhall/src/serde.rs
index bc76c49..96bc765 100644
--- a/dhall/src/serde.rs
+++ b/dhall/src/serde.rs
@@ -11,7 +11,7 @@ impl<'a, T: serde::Deserialize<'a>> Deserialize<'a> for T {
     }
 }
 
-struct Deserializer<'a>(Cow<'a, SubExpr<Label, X, X>>);
+struct Deserializer<'a>(Cow<'a, SubExpr<X, X>>);
 
 impl serde::de::Error for Error {
     fn custom<T>(msg: T) -> Self
diff --git a/dhall/src/traits/static_type.rs b/dhall/src/traits/static_type.rs
index c3f323b..f90b8df 100644
--- a/dhall/src/traits/static_type.rs
+++ b/dhall/src/traits/static_type.rs
@@ -32,7 +32,7 @@ pub trait SimpleStaticType {
     fn get_simple_static_type() -> SimpleType;
 }
 
-fn mktype(x: SubExpr<Label, X, X>) -> SimpleType {
+fn mktype(x: SubExpr<X, X>) -> SimpleType {
     x.into()
 }
 
@@ -106,22 +106,22 @@ impl SimpleStaticType for String {
 
 impl<A: SimpleStaticType, B: SimpleStaticType> SimpleStaticType for (A, B) {
     fn get_simple_static_type() -> SimpleType {
-        let ta: SubExpr<_, _, _> = A::get_simple_static_type().into();
-        let tb: SubExpr<_, _, _> = B::get_simple_static_type().into();
+        let ta: SubExpr<_, _> = A::get_simple_static_type().into();
+        let tb: SubExpr<_, _> = B::get_simple_static_type().into();
         mktype(dhall::subexpr!({ _1: ta, _2: tb }))
     }
 }
 
 impl<T: SimpleStaticType> SimpleStaticType for Option<T> {
     fn get_simple_static_type() -> SimpleType {
-        let t: SubExpr<_, _, _> = T::get_simple_static_type().into();
+        let t: SubExpr<_, _> = T::get_simple_static_type().into();
         mktype(dhall::subexpr!(Optional t))
     }
 }
 
 impl<T: SimpleStaticType> SimpleStaticType for Vec<T> {
     fn get_simple_static_type() -> SimpleType {
-        let t: SubExpr<_, _, _> = T::get_simple_static_type().into();
+        let t: SubExpr<_, _> = T::get_simple_static_type().into();
         mktype(dhall::subexpr!(List t))
     }
 }
@@ -142,8 +142,8 @@ impl<T: SimpleStaticType, E: SimpleStaticType> SimpleStaticType
     for std::result::Result<T, E>
 {
     fn get_simple_static_type() -> SimpleType {
-        let tt: SubExpr<_, _, _> = T::get_simple_static_type().into();
-        let te: SubExpr<_, _, _> = E::get_simple_static_type().into();
+        let tt: SubExpr<_, _> = T::get_simple_static_type().into();
+        let te: SubExpr<_, _> = E::get_simple_static_type().into();
         mktype(dhall::subexpr!(< Ok: tt | Err: te>))
     }
 }
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 63041bb..8b7f011 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -14,16 +14,13 @@ use dhall_syntax::*;
 
 use self::TypeMessage::*;
 
-type InputSubExpr = SubExpr<Label, Span, Normalized>;
-type OutputSubExpr = SubExpr<Label, X, X>;
-
 impl Resolved {
     pub fn typecheck(self) -> Result<Typed, TypeError> {
         type_of(self.0)
     }
     pub fn typecheck_with(self, ty: &Type) -> Result<Typed, TypeError> {
-        let expr = self.0;
-        let ty = ty.to_expr().embed_absurd().note_absurd();
+        let expr: SubExpr<_, _> = self.0;
+        let ty: SubExpr<_, _> = ty.to_expr().embed_absurd().note_absurd();
         type_of(expr.rewrap(ExprF::Annot(expr.clone(), ty)))
     }
     /// Pretends this expression has been typechecked. Use with care.
@@ -46,7 +43,7 @@ impl Typed {
 }
 
 impl Normalized {
-    fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         Normalized(self.0.shift(delta, var))
     }
     pub(crate) fn to_type(self) -> Type {
@@ -58,7 +55,7 @@ impl Type {
     pub(crate) fn to_normalized(&self) -> Normalized {
         self.0.to_normalized()
     }
-    pub(crate) fn to_expr(&self) -> OutputSubExpr {
+    pub(crate) fn to_expr(&self) -> SubExpr<X, X> {
         self.0.to_expr()
     }
     pub(crate) fn to_value(&self) -> Value {
@@ -76,10 +73,10 @@ impl Type {
     fn internal_whnf(&self) -> Option<Value> {
         self.0.whnf()
     }
-    pub(crate) fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+    pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         Type(self.0.shift(delta, var))
     }
-    pub(crate) fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
+    pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
         Type(self.0.subst_shift(var, val))
     }
 
@@ -127,7 +124,7 @@ impl TypeInternal {
     fn to_normalized(&self) -> Normalized {
         self.to_typed().normalize()
     }
-    fn to_expr(&self) -> OutputSubExpr {
+    fn to_expr(&self) -> SubExpr<X, X> {
         self.to_normalized().to_expr()
     }
     fn to_value(&self) -> Value {
@@ -151,14 +148,14 @@ impl TypeInternal {
             _ => None,
         }
     }
-    fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         use TypeInternal::*;
         match self {
             Typed(e) => Typed(Box::new(e.shift(delta, var))),
             Const(c) => Const(*c),
         }
     }
-    fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
+    fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
         use TypeInternal::*;
         match self {
             Typed(e) => Typed(Box::new(e.subst_shift(var, val))),
@@ -176,12 +173,12 @@ impl PartialEq for TypeInternal {
 
 #[derive(Debug, Clone)]
 pub(crate) enum EnvItem {
-    Type(Var<Label>, Type),
+    Type(V<Label>, Type),
     Value(Normalized),
 }
 
 impl EnvItem {
-    fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         use EnvItem::*;
         match self {
             Type(v, e) => Type(v.shift(delta, var), e.shift(delta, var)),
@@ -208,8 +205,8 @@ impl TypecheckContext {
     pub(crate) fn insert_value(&self, x: &Label, t: Normalized) -> Self {
         TypecheckContext(self.0.insert(x.clone(), EnvItem::Value(t)))
     }
-    pub(crate) fn lookup(&self, var: &Var<Label>) -> Option<Cow<'_, Type>> {
-        let Var(x, n) = var;
+    pub(crate) fn lookup(&self, var: &V<Label>) -> Option<Cow<'_, Type>> {
+        let V(x, n) = var;
         match self.0.lookup(x, *n) {
             Some(EnvItem::Type(_, t)) => Some(Cow::Borrowed(&t)),
             Some(EnvItem::Value(t)) => Some(t.get_type()?),
@@ -241,12 +238,8 @@ fn function_check(a: Const, b: Const) -> Result<Const, ()> {
     }
 }
 
-fn match_vars(
-    vl: &Var<Label>,
-    vr: &Var<Label>,
-    ctx: &[(&Label, &Label)],
-) -> bool {
-    let (Var(xL, mut nL), Var(xR, mut nR)) = (vl, vr);
+fn match_vars(vl: &V<Label>, vr: &V<Label>, ctx: &[(&Label, &Label)]) -> bool {
+    let (V(xL, mut nL), V(xR, mut nR)) = (vl, vr);
     for &(xL2, xR2) in ctx {
         match (nL, nR) {
             (0, 0) if xL == xL2 && xR == xR2 => return true,
@@ -272,8 +265,8 @@ where
     use dhall_syntax::ExprF::*;
     fn go<'a, S, T>(
         ctx: &mut Vec<(&'a Label, &'a Label)>,
-        el: &'a SubExpr<Label, S, X>,
-        er: &'a SubExpr<Label, T, X>,
+        el: &'a SubExpr<S, X>,
+        er: &'a SubExpr<T, X>,
     ) -> bool
     where
         S: ::std::fmt::Debug,
@@ -357,9 +350,9 @@ fn type_of_const(c: Const) -> Result<Type, TypeError> {
     }
 }
 
-fn type_of_builtin(b: Builtin) -> InputSubExpr {
+fn type_of_builtin<E>(b: Builtin) -> Expr<X, E> {
     use dhall_syntax::Builtin::*;
-    rc(match b {
+    match b {
         Bool | Natural | Integer | Double | Text => dhall::expr!(Type),
         List | Optional => dhall::expr!(
             Type -> Type
@@ -439,8 +432,7 @@ fn type_of_builtin(b: Builtin) -> InputSubExpr {
         OptionalNone => dhall::expr!(
             forall (A: Type) -> Optional A
         ),
-    })
-    .note_absurd()
+    }
 }
 
 macro_rules! ensure_equal {
@@ -627,7 +619,10 @@ impl TypeIntermediate {
 
 /// Takes an expression that is meant to contain a Type
 /// and turn it into a type, typechecking it along the way.
-fn mktype(ctx: &TypecheckContext, e: InputSubExpr) -> Result<Type, TypeError> {
+fn mktype(
+    ctx: &TypecheckContext,
+    e: SubExpr<Span, Normalized>,
+) -> Result<Type, TypeError> {
     Ok(type_with(ctx, e)?.to_type())
 }
 
@@ -650,7 +645,7 @@ enum Ret {
 /// succeeded, or an error if type-checking failed
 fn type_with(
     ctx: &TypecheckContext,
-    e: InputSubExpr,
+    e: SubExpr<Span, Normalized>,
 ) -> Result<Typed, TypeError> {
     use dhall_syntax::ExprF::{
         Annot, App, Embed, Lam, Let, OldOptionalLit, Pi, SomeLit,
@@ -761,7 +756,7 @@ fn type_last_layer(
                 mkerr(TypeMismatch(f.clone(), tx.clone().to_normalized(), a))
             });
 
-            Ok(RetType(tb.subst_shift(&x.into(), &a)))
+            Ok(RetType(tb.subst_shift(&V(x.clone(), 0), &a)))
         }
         Annot(x, t) => {
             let t = t.to_type();
@@ -942,7 +937,9 @@ fn type_last_layer(
             }
         }
         Const(c) => Ok(RetTyped(const_to_typed(c))),
-        Builtin(b) => Ok(RetType(mktype(ctx, type_of_builtin(b))?)),
+        Builtin(b) => {
+            Ok(RetType(mktype(ctx, rc(type_of_builtin(b)).note_absurd())?))
+        }
         BoolLit(_) => Ok(RetType(builtin_to_type(Bool)?)),
         NaturalLit(_) => Ok(RetType(builtin_to_type(Natural)?)),
         IntegerLit(_) => Ok(RetType(builtin_to_type(Integer)?)),
@@ -1001,7 +998,7 @@ fn type_last_layer(
 /// `typeOf` is the same as `type_with` with an empty context, meaning that the
 /// expression must be closed (i.e. no free variables), otherwise type-checking
 /// will fail.
-fn type_of(e: InputSubExpr) -> Result<Typed, TypeError> {
+fn type_of(e: SubExpr<Span, Normalized>) -> Result<Typed, TypeError> {
     let ctx = TypecheckContext::new();
     let e = type_with(&ctx, e)?;
     // Ensure `e` has a type (i.e. `e` is not `Sort`)
@@ -1012,7 +1009,7 @@ fn type_of(e: InputSubExpr) -> Result<Typed, TypeError> {
 /// The specific type error
 #[derive(Debug)]
 pub(crate) enum TypeMessage {
-    UnboundVariable(Var<Label>),
+    UnboundVariable(V<Label>),
     InvalidInputType(Normalized),
     InvalidOutputType(Normalized),
     NotAFunction(Typed),