leftover constraints on irrelevant variables

[ooovi]

 function test()          
    function f(a)         
        function h(b)     
            i(b) = 2*b + a
            i(b*5)        
        end               
        function g(h,a)   
            x = h(a*7)    
            y = h(a*7)    
            x + y         
        end               
        a = g(h,a)        
        a = g(h,a)        
        function h(b::Integer)     
            a*11          
        end               
        a = g(h,a)        
        a                 
    end                   
    f(13)                 
 end

gives the right result, but also has leftover constraint that don't appear in the result type:

Result: (Fun([([] -> NoFun(Num(Int[286.0]))) @ Just []]),

(...)

- constraints:
   - top:
constr_5 : [final,worst,global,exact,special] IsTypeOpResult (Binary + (Num(τ_43) @ η_8,Num(Int[13.0]) @ η_9) τr_17),
constr_6 : [final,worst,global,exact,special] IsTypeOpResult (Binary * (Num(Int[2.0]) @ η_10,τa_19 @ η_11) Num(τ_43)),
constr_7 : [final,worst,global,exact,special] IsTypeOpResult (Binary * (τa_23 @ η_12,Num(Int[5.0]) @ η_13) τa_19)

[MxmUrw]

The problem is that when checking a bunch of choices, we create constraints for all of them. And later, when we choose one of them, all the irrelevant constraints are left over.

This means we should keep track of which constraints belong to which choice, or alternatively, only really create those constraints once a choice is chosen.

[MxmUrw]

As of 018ed36e172d78906d3dd6489da1eb5064a3ffd4 we still have this problem.

[MxmUrw]

Implementation Idea

1. The function type has a unique identifier (probably tree-structured)
2. When checking a function we create a new such identifier
3. All constraints which occur during checking know that they belong to this checking-instance
4. When discharging IFAs, we look at the identifiers of all choices which were not chosen and discharge the constraints belonging to them