One perhaps-interesting use case might be to use the fastest possible solver in the case of compiling generated/foreign code, so basically code that's expected

One perhaps-interesting use case might be to use the fastest possible solver in the case of compiling generated/foreign code, so basically code that's expected to always compile (but which still needs to be checked for safety). One could even imagine using it as a first-pass for code and to just fall back to a slower-but-with-better-error-messages type checker if errors are found. (Of course you'd end up with two orthogonal implementations of the type checker, but that might not even be a bad thing since you'd be easily able to check for inconsistencies between them, aka. type checker bugs.)