If a set of ability variables always appears together, combine them

[pchiusano]

We managed to infer the following type:

Seq.fromListAt :
  ∀ g h3 h2 h1 h a k.
    Location {g, h3, h2, h1, h, h1, h} -> Nat -> [a] ->{h2, h1, h} Seq k a

Notice that {h, h1, h2} are always together in the inferred type. So we might as well just call that parameter h. They are also duplicated.

Deduplicated and coalesced, we get the nice type

Seq.fromListAt :
    Location {g, h} -> Nat -> [a] ->{h} Seq k a

Which is something a human might write.

I'd say this isn't super high priority, but it'd be a nice win for the inference algorithm. The more times that inference gives something sensible the better.

[dolio]

Yeah, I kind of wonder how many type errors of the multiple variable sort are caused by inferring this sort of type for intermediate steps.

[pchiusano]

Totally.

[pchiusano]

I just noticed that h3 appears on the Location but not in the result.

But applying the same simplification rule again, the variable set {g, h3} is never separated elsewhere in the signature, so we might as well just call that g, which yields the desired signature.