The use of genOf/instOf can be unsound if constraints are solved in a certain order. The issue is that a variable ty might be implicitly active if it appears in the solution for d : T(ty), and another constraint d : T' (where ty not in T') exists. Generalization might happen before the unification. This is caught at runtime, so unsound results are never returned, but than analysis fails altogether.

Possible solutions might be:

1. Make {x} : ty and d : ty different constraints (much like graph and resolution). Solve {x} : ty as assumptions, and d : ty as constraints. This would disallow inference from use to declaration.
2. Keep all variables in types active until all d : ty constraints are resolved. This will probably cause problems with TDNR, because d : ty depends on resolution, which might not succeed if a genOf is somewhere in the chain.

Solution 1 seems more flexible, but still might inhibit inference in method bodys which is desirable.

Submitted by Hendrik van Antwerpen on 24 June 2017 at 19:10