When I say

type 'a t = 'a foo foo
and 'a foo = int constraint 'a = int

ocaml says

File "scratch.ml", line 1, characters 0-22:
1 | type 'a t = 'a foo foo
    ^^^^^^^^^^^^^^^^^^^^^^
Error: Constraints are not satisfied in this type.
       Type int should be an instance of 'a foo
       foo is abstract because no corresponding cmi file was found in path.

But this program should be accepted, I think, with something like this signature:

type 'a t = int constraint 'a = int
type 'a foo = int constraint 'a = int

I think the problem is that Typedecl.check_regularity uses the orig_env when checking arguments -- but the orig_env doesn't know that 'a foo is an abbreviation for int when checking the manifest of t. I don't know enough of what's going on here to suggest a fix. But even if a proper fix is out of reach, the error message definitely has room for improvement: int is an instance of 'a foo (because they're equal) and there is no missing cmi file involved.