Fix GADT casting when typing if expressions

[Linyxus]

Fixes #14776.

Currently, when typing if expressions the compiler computes the union type of the two branches, during which GADT constraints may be implicitly used. This cause -Ycheck to fail due to the missing of proper GADT casts. The problems caused by this can be classified into two cases:

• In the first case, GADT casts are inserted in the branches, but the cast does not contain enough typing information to recover the type of the if tree when checking the tree. Details of this case are discussed in Refine GADT casts with GADT approximation of singleton types #15533.

• In the second case, no GADT cast is inserted. The tree fails the checker due to the lack of GADT casts. For example:

  trait Expr[T]
  case class IntExpr() extends Expr[Int]
  
  def flag: Boolean = ???
  
  def foo[T](ev: Expr[T]): Int | T = ev match
    case IntExpr() =>
      if flag then
        val i: T = ???
        i
      else
        (??? : Int)

  The if tree is typed as T | Int which get simplified to T with GADT constraints, with no GADT cast inserted. Later the checker finds that T | Int does not confirm to T (w/o GADT constr) and fails.

This PR fixes this issue by doing two things:

• Change 1: When typing an if expression if cond then thenp else elsep, we will compare thenp.tpe and elsep.tpe to the type assigned to the if tree, which is thenp.tpe | elsep.tpe. If thenp/elsep.tpe is a subtype of thenp.tpe | elsep.tpe only when GADT constraint is used, we will insert a GADT cast to ensure -Ycheck passes in future phases. With this change, when typing the above example we will insert a cast (??? : Int).$asInstanceOf[T].

• Change 2: We cherry-pick the related commit in Refine GADT casts with GADT approximation of singleton types #15533 to refine the cast with GADT approximated type when the casted tree is a singleton. For the example in If expressions typed with GADT constraints cause failure with -Ycheck:all #14776:

  trait T1
  trait T2 extends T1
  
  trait Expr[T] { val data: T = ??? }
  case class Tag2() extends Expr[T2]
  
  def flag: Boolean = ???
  
  def foo[T](e: Expr[T]): T1 = e match {
    case Tag2() =>
      if flag then
        new T2 {}
      else
        e.data
  }

  We will insert a cast e.data.$asInstanceOf[e.data.type & T2] (instead of e.data.$asInstanceOf[e.data.type & T1]). With only change 1, we will insert two GADT casts like e.data.$asInstanceOf[e.data.type & T1].$asInstanceOf[T2] for this example, which is wordy and loses the identity of e.data. So change 2 makes sure the cases involving GADT casts will be solved, and change 1 takes care of the rest.

[dwijnand]

Very nicely done and explained!

[Linyxus]

Just confirmed that: with this fix, the path-dependent GADT branch (#14754) passes the test which was broken previously in the bootstrapped-only compilation testsuite.

[abgruszecki]

@Linyxus I'll take a detailed look at this PR tomorrow, but one thing I want to mention right now is that it'd be best to link this PR from the piece of code you changed in Typer. This is a very subtle fix and we don't want the discussion (and your explanation!) to get lost.

[dwijnand]

I was considering whether we should push this logic into assignType(If... But we're already rolling our own here, by assigning the type after calling the tree copier.

[Linyxus]

Yes, it seems that the original code is the only callsite of assignType(If... (not fully verified since metals often lies to me ;)). It would be good to push the logic into assignType.

[Linyxus]

But it seems that pushing this logic into TypeAssigner will require us to also refactor the methods related to GADT casts (gadtAdaptBranch and Typer.insertGadtCast) into TypeAssigner. I am not sure whether it is good to put them there.

[dwijnand]

Yes, it seems that the original code is the only callsite of assignType(If... (not fully verified since metals often lies to me ;)).

There's also the calls from tpd. The top-level defs If and InlineIf, and the If in the tree copier.

In terms of pushing logic, I was quite surprised to find some not-plain-basic code in TypeAssigner in assignType(Apply..) which is called by innocent-looking tpd.Apply(..) (code to do with substituting type parameters). So now I'm not sure if it's better to continue to hide away your logic here for whenever an If is constructed or copied, or whether it's best to break the convention and not move it... 🤔

[dwijnand]

@abgruszecki do you hold an opinion on this?

[Linyxus]

Ok! I will quickly mention it during the lab meeting.
Edit: just realized that I mistaken the time of the lab meeting. I thought Alex was saying that I could raise the topic during the capture calculus meeting (but it is actually on Friday). I guess Alex is actually talking to @dwijnand? :P

[abgruszecki]

Yep yep, I am talking about the Thursday meeting @ 15:00.

[dwijnand]

You should come to the meeting on Thursday and raise it! 😄 (Or I can, np)

[Linyxus]

I'd be glad to join this lab meeting but Thursday 15:00 this week does not work well for me. :( I will appreciate knowing the results of your discussion on this topic! :D

[dwijnand]

Martin raised a good point: seeing as this involves GADT information, that doesn't survive post typing, there's little sense to put it in a more general place like TypeAssigners: leaving it in Typer makes sense.

[abgruszecki]

Compiler design aside, the code changes LGTM. Great job with the analysis and explanation, @Linyxus!

[abgruszecki]

I'm not really familiar with the compiler architecture around these areas. Are you saying that in general it would be good for this logic to be in TypeAssigner, but then some special-case logic there can sometimes be surprising as well?

[abgruszecki]

Maybe it'd be best to quickly raise the topic during the Thursday meeting, if you think it makes sense.