 								.map { _ in body.out.substitute(i, b) }
 						},
 						otherwise: const(Either.Left("illegal application of \(a) : \(A) to \(b)")))
-				}
+				})
 
 		case let .Projection(term, branch):
-			return term.inferType(context)
+			return annotate(term.inferType(context)
 				.flatMap { type in
 					type.analysis(
 						ifLambda: { i, A, B in
 							Either.Right(branch ? B.out.substitute(i, A.out) : A.out)
 						},
 						otherwise: const(Either.Left("illegal projection of field \(branch ? 1 : 0) of non-product value \(term) of type \(type)")))
-				}
+				})
 
 		case let .Annotation(term, type):
-			return term.checkType(type, context: context)
-				.map(const(type))
+			return annotate(term.checkType(type, context: context)
+				.map(const(type)))
 
 		case let .Axiom(_, type):
 			return Either.right(type)

			return .right(.BooleanType)

		case let .If(condition, then, `else`):
			return condition.checkType(.BooleanType, context: context)
				>> (then.inferType(context) &&& `else`.inferType(context))
					.map { a, b in
						a == b
							? a
							: Expression.lambda(Recur(.BooleanType)) { Recur(.If($0, Recur(a), Recur(b))) }
					}

		case .UnitType, .BooleanType:
			return .right(.Type(0))

			return .right(.Type(n + 1))

		case let .Variable(i):
			return annotate(context[i].map(Either.Right) ?? Either.Left("Unexpectedly free variable \(i)"))

		case let .Lambda(i, type, body):
			return annotate(type.checkIsType(context)
				>> body.inferType(context + [ .Local(i): type ])
					.map { Expression.lambda(Recur(type), const(Recur($0))) })

		case let .Product(a, b):
			return annotate((a.inferType(context) &&& b.inferType(context))
				.map { A, B in Expression.lambda(Recur(A), const(Recur(B))) })

		case let .Application(a, b):
			return annotate(a.inferType(context)
				.flatMap { A in
					A.analysis(
						ifLambda: { i, type, body in
