Couldn’t the comparison (and also the fast path I guess) just be putting all the inference passes into a single big pass, which then avoids the quadratic number of re-applications of passes? Looks like unification is otherwise the same?
replyThis is what I was thinking too. Just do a single unification pass, but track the provenance of each type assignment. If an error is needed, use the provenances of the colliding unifications to decide which context locations to prioritize.
reply