Connect the subtyping layers in a different way (for supremum)

[MxmUrw]

Currently, we have a function convertSubtypingToSupremum which builds a supremum from multiple subtyping constraints.
This is needed because when resolving suprema using the subtyping graph, we forget that stuff was a supremum, and construct subtyping constraints from that. Which later are turned into suprema by that function.

This is quite unsatisfactory, since information is lost. It would be best, if we would do this directly.

For example, discharging bot/top constraints has now to be done in a later phase (59b66f0), to make sure that the supremum restoration runs before it. Even in that later phase, the question whether all restorations happen as supposed is not quite clear.

[MxmUrw]

Even though this seems to be hacky, our existing examples never actually failed because of this problem. So this is not high priority.

[MxmUrw]

We now have an example in which our adhoc solution failes.

Description

Currently our procedure is very ad-hoc. During supremum solving subtyping constraints are created, which are then reintegrated into a supremum constraint here.

The problem is that this is not done always (as in this location of execution we do not have the information about where a given set of subtyping constraints came from, and we have to restrict ourselves to cases where we know that we do not break other constraints - i.e. when the RHS does not occur in other constraints).

The Problematic example

As seen in the following example though, there are situations we do not reconstruct even though we should.

Example:

julia> typecheck_hs_from_string_detailed("module F
        function test()       
          a = 3               
          b = 5               
          function f(a,b)     
            a1 = 7            
            function g(ff)    
              (a,b) -> ff(a,b)
            end               
            function h(a,b)   
              b1 = 3          
              a + b1          
            end               
            g(h)(a1,b)        
          end                 
          y = b + 12          
          b2 = 9              
          x = a               
          a2 = 12             
          f(x,y)              
        end                 
         end                 

       ")

Log:

               [Solver]: solving (exact) constr_35 : IsSupremum (IR Int,IR Int) :=: τ_21
                            - CREATE constr_43 : IsLessEqual (τ_27,τ_28)
                            - SUB τ_27 := Int
                            - SUB τ_21 := IR τ_28
                            - CREATE constr_44 : IsLessEqual (τ_29,τ_30)
                            - SUB τ_29 := Int
                            - SUB τ_30 := τ_28
                            - DISCHARGE constr_35
                         => Discharged
               [Solver]: solving (worst) constr_3 : MakeNonConst (Fun([([NoFun(Num(IR Int[7.0 ©])) @ ∑∅,NoFun(Num(IR τ_24[17.0 ©])) @ ∑∅] -> NoFun(Num(IR τ_28[10.0 ©]))) @ Nothing]),worst)
                            - DISCHARGE constr_3
                         => Discharged
               [Solver]: solving (worst) constr_6 : MakeNonConst (NoFun(Num(IR τ_24[17.0 ©])),worst)
                            - DISCHARGE constr_6
                         => Discharged
               [Solver]: solving (worst) constr_10 : MakeNonConst (NoFun(Num(IR τ_24[17.0 ©])),worst)
                            - DISCHARGE constr_10
                         => Discharged
               [Solver]: solving (worst) constr_2 : MakeNonConst (NoFun(Num(IR τ_24[17.0 ©])),worst)
                            - DISCHARGE constr_2
                         => Discharged
               [Solver]: solving (worst) constr_5 : MakeNonConst (NoFun(Num(IR Int[7.0 ©])),worst)
                            - DISCHARGE constr_5
                         => Discharged
               [Solver]: solving (worst) constr_9 : MakeNonConst (NoFun(Num(IR Int[3.0 ©])),worst)
                            - DISCHARGE constr_9
                         => Discharged
               [Solver]: solving (worst) constr_1 : MakeNonConst (NoFun(Num(IR Int[7.0 ©])),worst)
                            - DISCHARGE constr_1
                         => Discharged
               [Solver]: solving (final) constr_41 : IsLessEqual (Int,τ_24)
                            - DISCHARGE constr_41
                         => Discharged
               [Solver]: solving (final) constr_43 : IsLessEqual (Int,τ_28)
                            - DISCHARGE constr_43
                         => Discharged
               [Solver]: solving (final) constr_42 : IsLessEqual (Int,τ_24)
                            - DISCHARGE constr_42
                         => Discharged
               [Solver]: solving (final) constr_44 : IsLessEqual (Int,τ_28)
                            - DISCHARGE constr_44
                         => Discharged
======================== End LOG =====================
======================== Errors =====================

======================== End Errors =====================

---------------------------------------------------------------------------
Type:
Fun([([] -> NoFun(Num(IR τ_28[10.0 ©]))) @ Just []])
---------------------------------------------------------------------------

The constraints constr_43 and constr_44 created during solving of constr_35 should be reconstructed into a supremum constraint, but are not since the result-variable τ_28 also occurs in constr_3. And when constr_3 is solved, we are already at a too-late stage, and 43 and 44 are discharged since the LHS is a bottom on its subtyping-graph-level.

Idea

We want a proper connection of the subtyping levels.

[MxmUrw]

This seems to be too difficult to do properly. Our current system isn't that bad as well.