TypeVariable.nameHint lost in constraint solving and type simplification

[fo5for]

class Test[A]: { x: A }
    method Mth[B]: (A -> B) -> B
    method Mth[B] (f: A -> B) = f this.x
//│ Defined class Test
//│ Declared Test.Mth: Test['A] -> ('A -> 'B) -> 'B
//│ Defined Test.Mth: Test['A] -> ('A -> 'a) -> 'a

The name hint for the type parameter B in the method definition is lost. I have identified two sources of this issue:

1. nameHint is not preserved in extrusion
   

   mlscript/shared/src/main/scala/mlscript/ConstraintSolver.scala

   Line 392 in 9930721

   val nv = freshVar(tv.prov)(lvl)

   
   (That's a downside of providing default arguments. You are not forced to review every invocation and provide the appropriate argument...)

2. nameHint is not unified when simplifying polar variables
   Looking at the debug output of the above code snippet (after fixing 1.), the name hint is still present in the canonical inferred type:
   //│ Canon: ((test<> & {Test#A: (A31 -> A31), x: A31}) -> ((((A31 | α32) -> (α33 & B34)) & α35) -> α33))
   But it is later simplified away since it only cooccurs with α33 in one polarity:
   //│ [sub] α32 -> None, B34 -> None, α35 -> None

[LPTK]

Nice job tracing this to the root causes. I tried to fix it, but there is one more thing that's going wrong here. In fact I noticed that method type parameters don't seem to be treated correctly.

class C
  method Foo[A](a: A) = a + 1
//│ Defined class C
//│ Defined C.Foo: C -> int -> int

Here A should be treated as a rigid type variable (implemented as a trait tag). I'm looking into fixing it now.

(That's a downside of providing default arguments. You are not forced to review every invocation and provide the appropriate argument...)

Very true. They should be used sparingly!

[LPTK]

Man, the method typing code is quite hairy. I noticed it also performs some needless subsumption checks. It's in dire need of simplification (let's look at this in the next meeting).

[fo5for]

Man, the method typing code is quite hairy. I noticed it also performs some needless subsumption checks. It's in dire need of simplification (let's look at this in the next meeting).

Right... The unnecessary subsumption checks can be skipped with a guard. But ultimately refactoring should be the way to go.