Logic subtyping and overloading

[auht]

2025-02-26 TODO:

• [x] Add spaces like a civilized person
• [x] Check intersections for WFedness
• [x] Remove assumption that only the first argument needs disjointness
  • [x] Deal with nested dss
• [x] Support generalization (update collectTVs)
• [x] Add records ~~(for now use temporary syntax fun foo: ["x": Int, "y": Int])~~

2025-03-06 TODO:

• [ ] don't duplicate when LB is TV on same or higher level, in which case you can make both vars bound each other (same level) or the other one bound the LB
• [ ] properly update type simplifier (and remove kludge)
• [x] remove use of nondeterministic collections

Later:

• [ ] During simplification, take UBs into account to reduce things

2025-03-13 TODO:

Later:

• [ ] use different propagation rules for TVs of same level
• [ ] add an option to enable/disable :logicSub