Type inference has at least quadratic complexity because of immutability & bad algs.

[Blaisorblade]

I just realized that the repeated substitutions inside unification are quadratic, which seems bad, and hopefully can be improved upon. (Maybe this requires mutation for unification variables).

I imagine looking up type variables when matching them, and substituting them later, might be better (not sure, but the lookup is at least O(1), so it seems a matter of constant factors ).

Using mutation (and treating a resolved variable as the type it resolves too everywhere needed) might be an alternative.

[Toxaris]

See this email for some pointers about how to implement unification efficiently.

[Blaisorblade]

Thanks! 👍