## Typechecking should only use squaresubtype when checking a result type against an expected constraint

The typechecking function as the following signature:

`type_check loc env constr e`

where `loc`

is a location, env is the environment, `constr`

is an expected type and `e`

is the expression to type-check. It returns an expression `e'`

(where some expressions may have been modified, e.g. branch of patterns specialized, unneeded cast removed etc.) and an output type `t`

. The last thing it often does before returning is:

`verify loc t constr`

which checks that indeed, `t`

is a subtype of the expected constraint `constr`

(for instance, when typing the body of a function, the constraint is the expected result type of the function). `verify`

uses plain subtyping which is wrong. It should:
use `squaresubtype_delta`

to check if there exists substitutions s1,...,sn such that t < constr
return not, t but t{s1} & ... & t{sn}
Note that because typechecking is half half between the old monomorphic code and the new polymorphic code (buggy) we end up with either weird type error or even unsound and clearly ill-typed code that compiles:

```
let f (<bar>['a] -> <foo>['a]) <bar>[ x ] -> <foo>[x]
;;
let f (<bar>['a] -> <foo>['a]) <bar>[ y ] -> <foo>[ y]
in
let apply (x : 'b) : 'b =
f x
;;
```

the body of apply is clearly wrong yet it compiles with the current master.
We need to thoroughly review the code of `type_check`

(and other functions) to check for the following:

check everywhere there is an instance of

`Types.subtype`

to see whether`Types.squaresubtype`

should be used instead.properly review how the generalisation/freshening of type variables is done