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 whetherTypes.squaresubtype
should be used instead. -
properly review how the generalisation/freshening of type variables is done