Revert "Make SubExpr generic in the variable labels type"

This reverts commit 4c159640e5ee77ffa48b85a5bffa56350cf933ef.

1 files changed, 31 insertions, 34 deletions

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),