 							return .Right(type)
 						}
 
-						return .Left("Type mismatch: expected \(String(reflecting: self)) to be of type \(String(reflecting: against)), but it was actually of type \(String(reflecting: type)) in environment \(environment)")
+						return .Left("Type mismatch: expected \(String(reflecting: self)) to be of type \(String(reflecting: against)), but it was actually of type \(String(reflecting: type)) in environment \(context)")
 					}
 			}
 	}

				}

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

	public func typecheck(environment: [Name: Expression], against: Expression) -> Either<Error, Expression> {
		return (against.isType
				? Either.Right(against)
				: against.typecheck(environment, against: .Type(0)))
			.map { _ in against.evaluate() }
			.flatMap { against in
				typecheck(environment)
					.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(environment, against: .Type(0))
								.flatMap { _ in
									tag.out.typecheck(environment, against: tagType.out)
										.flatMap { _ in
											payload.out.typecheck(environment, against: body.out.substitute(i, tag.out))
												.map(const(type))
										}
								}

extension Expression where Recur: FixpointType, Recur: Equatable {
	// MARK: Typechecking

	public func typecheck(context: [Name: Expression] = [:]) -> Either<Error, Expression> {
		switch destructured {
		case .Unit:
			return .right(.UnitType)
