 			return type.typecheck(environment, against: .Type(0))
 				.flatMap { _ in
 					body.typecheck(environment + [ .Local(i): type ])
-						.map { Expression.lambda(type, const($0)) }
+						.map { Expression.lambda(Recur(type), const(Recur($0))) }
 			}
 
 		case let .Product(a, b):
 			return (a.typecheck(environment) &&& b.typecheck(environment))
-				.map { A, B in Expression.lambda(A, const(B)) }
+				.map { A, B in Expression.lambda(Recur(A), const(Recur(B))) }
 
 		case let .Application(a, b):
 			return a.typecheck(environment)

						.map { a, b in
							a == b
								? a
								: Expression.lambda(.BooleanType) { Expression.If($0, Recur(a), Recur(b)) }
						}
				}


extension Expression where Recur: FixpointType {
	// MARK: Higher-order construction

	public static func lambda(type: Recur, _ f: Recur -> Recur) -> Expression {
		var n = 0
		let body = f(Recur { .Variable(.Local(n)) })
		n = body.out.maxBoundVariable + 1
		return .Lambda(n, type, body)
	}


