 extension Expression where Recur: FixpointType, Recur: Equatable {
 	// MARK: Typechecking
 
-	public func typecheck(environment: [Name: Expression] = [:]) -> Either<Error, Expression> {
+	public func typecheck(context: [Name: Expression] = [:]) -> Either<Error, Expression> {
 		switch destructured {
 		case .Unit:
 			return .right(.UnitType)

			return .right(.BooleanType)

		case let .If(condition, then, `else`):
			return condition.typecheck(environment, against: .BooleanType)
				.flatMap { _ in
					(then.typecheck(environment) &&& `else`.typecheck(environment))
						.map { a, b in
							a == b
								? a

				}

		case let .Annotation(term, type):
			return term.typecheck(context, against: type)
				.map(const(type))
		}
	}

	public func typecheck(context: [Name: Expression], against: Expression) -> Either<Error, Expression> {
		return (against.isType
				? Either.Right(against)
				: against.typecheck(context, against: .Type(0)))
			.map { _ in against.evaluate() }
			.flatMap { against in
				typecheck(context)
					.map { $0.evaluate() }
					.flatMap { (type: Expression) -> Either<Error, Expression> in
						if case let (.Product(tag, payload), .Lambda(i, tagType, body)) = (self, against) {
							return tagType.out.typecheck(context, against: .Type(0))
								.flatMap { _ in
									tag.out.typecheck(context, against: tagType.out)
										.flatMap { _ in
											payload.out.typecheck(context, against: body.out.substitute(i, tag.out))
												.map(const(type))
										}
								}
