Use generic types in call to subtype

[goldfirere]

This is a small change within the type-checker to use generic-level types in the call to subtype, used to implement the :> operator.

The change here causes no known change in behavior. However, in Jane Street's branch, we sometimes use information about whether a type in principally known to make decisions about which modes to pay attention to; this change does make a differece in that branch. The reason I'm posting it here is that I think this small change in the code makes it a bit more semantically correct: the types in question are written by the user and therefore really should be treated at generic-level.

I think @garrigue is the right reviewer for this.

[goldfirere]

@garrigue and I discussed last week, and my sense at the time was that this patch looked good to him. @garrigue, are you ready to Approve? Thanks!

[garrigue]

The code is modified the way we discussed, giving the improved behavior on single coercions.
The modified output for recursive types is a bit confusing, but the types are semantically equivalent. Eventually it may be worth defining better the amount of unsharing caused by annotations.