Hindley-Milner type inference for language with implicit type casting

Question

I've only implemented the HM algorithm on a small academic language with a few primitive types and functions. In that case, the unification algorithm would return a type error if two different primitive types were given. For example, if statements unify their condition with primitive type bool, producing the following results:

if (true) ... // type safe
if ("5") // type error, cannot unify string and bool

I've now been tasked to implement a type inference algorithm on a language that allows type casting on primitive types. For example, one cast is int -> bool such that if(5) ... is now a valid expression.

The problem is, I can't figure out how to adapt the unify algorithm. Specifically, I'm stuck on dealing with the one directional nature of type casts, e.g. int -> bool is defined, but bool -> int is not. The unify algorithm has no notion of direction. Unifying type a and type b is the same as unifying type b and type a. So in the case of the if statement, if I say that unify int with bool is allowed, then unify bool and int must also be allowed, and suddenly the statement true + false is type safe.

I've searched for details of existing type systems that do this, but unfortunately I've only found resources that either show a basic HM inference algorithm similar to the first one I implemented, or are completely off topic.

Answer 1

Hindley-Milnor type inference doesn't support implicit type casting, so you can't fix that easily. You'd need a fundamentally different algorithm for type inference, and I'm not sure whether such a thing exists. I think there are ways to handle type inference with implicit type casts if you don't care about supporting polymorphic types, but as far as I know, the combination of polymorphic types, type inference, recursion, and implicit type casts is hard to handle simultaneously.

In contrast, it's straightforward to extend HM type inference to handle explicit type casting.