Simplification bug with methods and type parameters

[fo5for]

Discovered in c87010fca5f0f2742ab5d56aed7f5831f9af5ad0.

:NoJS

class Some[a]: { val: a }
  method Get: a
//│ Defined class Some[+a]
//│ Declared Some.Get: Some['a] -> 'a

// simplification bug here
def g x = (x.Get 0, x.Get "a")
//│ g: Some[nothing -> ('a | 'b)] -> ('b, 'a,)

g (error: Some[nothing -> 0])
//│ ╔══[ERROR] Type mismatch in application:
//│ ║  l.12:    g (error: Some[nothing -> 0])
//│ ║           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
//│ ╟── string literal of type `"a"` does not match type `nothing`
//│ ║  l.9:     def g x = (x.Get 0, x.Get "a")
//│ ║                                     ^^^
//│ ╟── Note: constraint arises from type reference:
//│ ║  l.12:    g (error: Some[nothing -> 0])
//│ ╙──                        ^^^^^^^
//│ res: (0, 0,) | error

// expected behavior
def g (x: Some['a]) = (x.val 0, x.val "a")
//│ g: Some["a" -> 'a & 0 -> 'b] -> ('b, 'a,)

g (error: Some[nothing -> 0])
//│ ╔══[ERROR] Type mismatch in application:
//│ ║  l.28:    g (error: Some[nothing -> 0])
//│ ║           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
//│ ╟── string literal of type `"a"` does not match type `nothing`
//│ ║  l.25:    def g (x: Some['a]) = (x.val 0, x.val "a")
//│ ║                                                 ^^^
//│ ╟── Note: constraint arises from type reference:
//│ ║  l.28:    g (error: Some[nothing -> 0])
//│ ╙──                        ^^^^^^^
//│ res: (0, 0,) | error

In the first definition of g using x.Get, the inferred type is erroneously printed with a nothing. This appears to be a simplification bug since actually passing something of the function parameter type to g results in an error. The error message also refers to type "a", which does not appear in the printed type of g. The expected behavior should be identical to the second definition of g using x.val.

[LPTK]

Thanks for reporting. Do you want to try your hand on it? (After the POPL deadline ofc.) You can see what's going on using the debug-simplification command :ds.