diff options
Diffstat (limited to '')
-rw-r--r-- | dhall/src/semantics/phase/typecheck.rs | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 852f41b..15025c1 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -6,7 +6,7 @@ use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::context::TyCtx; use crate::semantics::phase::normalize::merge_maps; use crate::semantics::phase::Normalized; -use crate::semantics::{Binder, Value, ValueKind}; +use crate::semantics::{AlphaVar, Binder, Value, ValueKind}; use crate::syntax; use crate::syntax::{ Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, Span, @@ -385,15 +385,15 @@ fn type_last_layer( App(f, a) => { let tf = f.get_type()?; let tf_borrow = tf.as_whnf(); - let (x, tx, tb) = match &*tf_borrow { - ValueKind::Pi(x, tx, tb) => (x, tx, tb), + let (tx, tb) = match &*tf_borrow { + ValueKind::Pi(_, tx, tb) => (tx, tb), _ => return mkerr(NotAFunction(f.clone())), }; if &a.get_type()? != tx { return mkerr(TypeMismatch(f.clone(), tx.clone(), a.clone())); } - let ret = tb.subst_shift(&x.into(), a); + let ret = tb.subst_shift(&AlphaVar::default(), a); ret.normalize_nf(); RetTypeOnly(ret) } @@ -500,13 +500,12 @@ fn type_last_layer( ValueKind::UnionType(kts) => match kts.get(&x) { // Constructor has type T -> < x: T, ... > Some(Some(t)) => { - let x = ctx.new_binder(x); RetTypeOnly( tck_pi_type( ctx, - x.clone(), + ctx.new_binder(x), t.clone(), - r.under_binder(x), + r.under_binder(), )? ) }, @@ -719,8 +718,8 @@ fn type_last_layer( // Union alternative with type Some(Some(variant_type)) => { let handler_type_borrow = handler_type.as_whnf(); - let (x, tx, tb) = match &*handler_type_borrow { - ValueKind::Pi(x, tx, tb) => (x, tx, tb), + let (tx, tb) = match &*handler_type_borrow { + ValueKind::Pi(_, tx, tb) => (tx, tb), _ => { return mkerr(NotAFunction( handler_type.clone(), @@ -736,8 +735,9 @@ fn type_last_layer( )); } - // Extract `tb` from under the `x` binder. Fails is `x` was free in `tb`. - match tb.over_binder(x) { + // Extract `tb` from under the binder. Fails if the variable was used + // in `tb`. + match tb.over_binder() { Some(x) => x, None => return mkerr( MergeHandlerReturnTypeMustNotBeDependent, |