samvv
commented
1 year ago One thing we could do is to keep a cyclic list on each type that grows with each successful join with another type. That way, the cyclic list would eventually contain all the types that are the same. If we then would add a guard that this list may only grow when encountering a type that isn't 'the one' TCon, we would end up with partial lists that contain only the subset of the program that were inferred as equal but not necessarily as specifically the Int or the Bool.
Next, we need a mechanism where an Int from a constant expression 1 is not equal to an Int from e.g. a type reference. This requires the introduction of an intermediate type. In the simplest case, we just clone a TCon and assign a new node to it. Some flags would need to ensure that this TCon is different from the global TCon types we wish to avoid.
If we had such lists, then an unification error could retrieve the two conflicting cycles by inspecting the two original types that the solver requested to be unified.
The problem we're facing is that error messages often do not explain exactly what made the error occur. A small improvement would be to pick an arbitrary expression from one side of the equation, pick one from the other, and print these nodes out.