let foo k.
let bar l = k == l
bar True
bar 1
foo 1
Right now, this program correctly produces two error diagnostics. One for bar 1 and one for foo 1. Both inform that Int and Bool do not match.
The two diagnostics didn't have to be. If we first had unified k with Int and only then inferred bar True and bar 1, we would find that bar True was wrong and bar 1 correctly related k with the Int type, as foo 1 does. This means one less diagnostic by just reversing some steps.
More generally, the problem is how we can unify constraints in such a way that the produced diagnostics are of a minimal amount.
Solution: Tracking Unified Types
For finding the minimal amount of diagnostics, one solution would be to keep track of all types that unified with each other instead of setting it to the first one. If a type unified with Int and Bool then an error is printed and both are added to a set. When another constraint requires this same type to be Bool, no diagnostic message is generated because it is already in the set. If, however, a new type String unifies with this type then String is added to the set and a diagnostic message is again generated.
We explicitly store the types in a set and not a list because the order of the types must not matter. In the above example, unifying k first with Int or first with Bool should not affect the outcome of the inference.
This method ensures that only really unexpected type combinations are reported, while types that are somewhat expected (because the source indicates that they are used like that) are ignored. At the same time, enough type errors are reported such that the user has to fix all (hidden) typing errors in the program before (s)he can continue.
Problem
Consider the following program:
Right now, this program correctly produces two error diagnostics. One for
bar 1and one forfoo 1. Both inform thatIntandBooldo not match.The two diagnostics didn't have to be. If we first had unified
kwithIntand only then inferredbar Trueandbar 1, we would find thatbar Truewas wrong andbar 1correctly relatedkwith theInttype, asfoo 1does. This means one less diagnostic by just reversing some steps.More generally, the problem is how we can unify constraints in such a way that the produced diagnostics are of a minimal amount.
Solution: Tracking Unified Types
For finding the minimal amount of diagnostics, one solution would be to keep track of all types that unified with each other instead of setting it to the first one. If a type unified with
IntandBoolthen an error is printed and both are added to a set. When another constraint requires this same type to beBool, no diagnostic message is generated because it is already in the set. If, however, a new typeStringunifies with this type thenStringis added to the set and a diagnostic message is again generated.We explicitly store the types in a set and not a list because the order of the types must not matter. In the above example, unifying
kfirst withIntor first withBoolshould not affect the outcome of the inference.This method ensures that only really unexpected type combinations are reported, while types that are somewhat expected (because the source indicates that they are used like that) are ignored. At the same time, enough type errors are reported such that the user has to fix all (hidden) typing errors in the program before (s)he can continue.