 						otherwise: const(Either.Left("illegal projection of field \(branch ? 1 : 0) of non-product value \(term) of type \(type)")))
 				}
 
-		case let (.Annotation(term, type), .None):
+		case let .Annotation(term, type):
 			return term.typecheck(context, against: type)
 				.map(const(type))
 
-		case let (.Axiom(_, type), .None):
+		case let .Axiom(_, type):
 			return Either.right(type)
-
-		// Everything else is an error.
-		case let (_, .Some(x)):
-			return Either.left("Don’t know how to check \(self) against \(x).")
 		}
 	}
 

						otherwise: const(Either.Left("illegal application of \(a) : \(A) to \(b)")))
				}

		case let (.Projection(term, branch), .None):
			return term.typecheck(context)
				.flatMap { type in
					type.analysis(

						}
				}

		case .UnitType, .BooleanType:
			return .right(.Type(0))
		case let .Type(n):
			return .right(.Type(n + 1))

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

		case let .Lambda(i, type, body):
			return type.typecheck(context, against: .Type(0))
				.flatMap { _ in
					body.typecheck(context + [ .Local(i): type ])
						.map { Expression.lambda(Recur(type), const(Recur($0))) }
				}

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

		case let .Application(a, b):
			return a.typecheck(context)
				.flatMap { A in
					A.analysis(
