 						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(

		return typecheck(context)
	}

	public func typecheck(context: Context = [:]) -> Either<Error, Expression> {
		switch destructured {
		// Inference rules.
		case .Unit:
			return .right(.UnitType)
		case .Boolean:
			return .right(.BooleanType)

		case let .If(condition, then, `else`):
			return condition.typecheck(context, against: .BooleanType)
				.flatMap { _ in
					(then.typecheck(context) &&& `else`.typecheck(context))
