Stricter --MLish: no subtyping via has_type guards

[mtzguido]

No description provided.

[mtzguido]

This PR makes the --MLish --lax mode more strict by disabling smt_ok for check_subtyping queries in Rel. This find a couple more stray type errors and fixes the problem in #3151 which is now not accepted. Two things to note:

1- We will now reject stuff like coerce #a #b (x:a) : b = x. Note this means we cannot check prims in --MLish --lax mode because of heterogeneous equality and Pervasives due to coerce_eq. Our build avoids this, but manually running --MLish --lax will likely fail there are .checked.lax files for the library already.
2- We will now run into #65, where a nat & bool is not a int & bool. There are a few places in the compiler where this was happening, mostly because List.length returns a nat. Adding an : int annotation solves it.

Fixes #3151