GitLab

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