Since we get the type of an expression from the `typecheck`, we could validate it against a user-provided spec.