Match type with bounds fails to reduce

[dwijnand]

Is

sealed trait Foo[A, X <: A]

type FooX[F] = F match {
  case Foo[a, x] => x
}

type MyFoo = Foo[String, "hello"]

val hello: FooX[MyFoo] = "hello"

related? It gives the error:

Found:    ("hello" : String)
Required: FooX[MyFoo]

Even in 3.1.2-RC1.

Originally posted by @s5bug in #6697 (comment)

[dwijnand]

It says:

9 |val hello: FooX[MyFoo] = "hello"
  |                         ^^^^^^^
  |                      Found:    ("hello" : String)
  |                      Required: FooX[MyFoo]
  |
  |                      Note: a match type could not be fully reduced:
  |
  |                        trying to reduce  FooX[MyFoo]
  |                        failed since selector  MyFoo
  |                        does not match  case Foo[a, x] => x
  |                        and cannot be shown to be disjoint from it either.

I thought it might be the type alias indirection, but, no, it looks even worst when you inline MyFoo:

9 |val hello: FooX[Foo[String, "hello"]] = "hello"
 |                                        ^^^^^^^
 |                 Found:    ("hello" : String)
 |                 Required: FooX[Foo[String, ("hello" : String)]]
 |
 |                 Note: a match type could not be fully reduced:
 |
 |                   trying to reduce  FooX[Foo[String, ("hello" : String)]]
 |                   failed since selector  Foo[String, ("hello" : String)]
 |                   does not match  case Foo[a, x] => x
 |                   and cannot be shown to be disjoint from it either.

[SethTisue]

Just to actually write it down without the extra type alias, and without a singleton type involved either:

trait Foo[A, X <: A]
type FooX[F] = F match { case Foo[_, x] => x }
"": FooX[Foo[String, String]]

[SethTisue]

Dale is thinking about at least three possible solution paths. In decreasing order of generality:

• make the type comparer able to reduce Foo[?, ?]#A to ? instead of throwing up its hands
• change argForParam on NamedType (there's code in there that sees the bound but ignores it) (or not, Dale currently thinks not)
• improve tparamBounds inside typedArg inside typedAppliedTypeTree

With the third seeming most promising at the moment.

I don't have any gut feeling about the viability of the first two options, but the third seems very plausible to me. The existing code:

          def tparamBounds = tparam.paramInfoAsSeenFrom(tpt1.tpe.appliedTo(tparams.map(_ => TypeBounds.empty)))

seems plausibly unfinished/naïve, as if cases such as this ticket simply weren't considered

[dwijnand]

Realising that I want to replace uses of type parameters in the bounds (with type references of the fresh pattern symbols) is similar in nature to general substituters lead me to NamedType's argDenot which has lots of similar looking things.

[dwijnand]

This is what the subtype trace looks like:

==> reduce match type Foo[String, ("hello" : String)] match {   case Foo[a, x] => x } 1497850786?
  ==> match case [a, x <: Foo[?, ?]#A] =>> scala.runtime.MatchCase[Foo[a, x], x] vs Foo[String, ("hello" : String)]?
    ==> isSubType Foo[String, ("hello" : String)] <:< Foo[a, x]?

First checking the subtyping of arg a, both a <:< String and String <:< a because it's invariant:

      ==> isSubType a <:< String?
        ==> isSubType a <:< String?
          <== isSubType Any <:< String = false
          <== isSubType Nothing <:< String = true
        <== isSubType a <:< String = true
      <== isSubType a <:< String = true
      ==> isSubType String <:< a?
        ==> isSubType String <:< a?
          <== isSubType String <:< Nothing = false
        <== isSubType String <:< a = true
      <== isSubType String <:< a = true

Second checking the subtyping of arg x, first x <:< "hello":

      ==> isSubType x <:< ("hello" : String)?
        ==> isSubType Foo[?, ?]#A <:< ("hello" : String)?
          <== isSubType Any <:< ("hello" : String) (left is approximated) = false
        <== isSubType Foo[?, ?]#A <:< ("hello" : String) = false
        ==> isSubType ("hello" : String) <:< Foo[?, ?]#A?
          <== isSubType String <:< Foo[?, ?]#A (left is approximated) = false
        <== isSubType ("hello" : String) <:< Foo[?, ?]#A = false
        ==> isSubType Foo[?, ?]#A <:< ("hello" : String)?
          <== isSubType Any <:< ("hello" : String) (left is approximated) = false
        <== isSubType Foo[?, ?]#A <:< ("hello" : String) = false
        <== isSubType Nothing <:< Foo[?, ?]#A & ("hello" : String) = true
      <== isSubType x <:< ("hello" : String) = true

then "hello" <:< x:

      ==> isSubType ("hello" : String) <:< x?
        <== isSubType ("hello" : String) <:< Nothing = false
        ==> isSubType ("hello" : String) <:< Foo[?, ?]#A & ("hello" : String)?
          ==> isSubType ("hello" : String) <:< Foo[?, ?]#A?
            <== isSubType String <:< Foo[?, ?]#A (left is approximated) = false
          <== isSubType ("hello" : String) <:< Foo[?, ?]#A = false
        <== isSubType ("hello" : String) <:< Foo[?, ?]#A & ("hello" : String) = false
      <== isSubType ("hello" : String) <:< x = false

And therefore it fails:

    <== isSubType Foo[String, ("hello" : String)] <:< Foo[a, x] = false

It actually does a few more checks (haven't where these checks are from):

    ==> isSubType String <:< a?
      ==> isSubType String <:< a?
        <== isSubType String <:< Nothing = false
        <== isSubType String <:< Any = true
      <== isSubType String <:< a = true
    <== isSubType String <:< a = true
    ==> isSubType a <:< String?
      ==> isSubType a <:< String?
        <== isSubType Any <:< String = false
      <== isSubType a <:< String = true
    <== isSubType a <:< String = true
    ==> isSubType ("hello" : String) <:< x?
      <== isSubType ("hello" : String) <:< Nothing = false
      ==> isSubType ("hello" : String) <:< Foo[?, ?]#A?
        <== isSubType String <:< Foo[?, ?]#A (left is approximated) = false
      <== isSubType ("hello" : String) <:< Foo[?, ?]#A = false
    <== isSubType ("hello" : String) <:< x = false

and then fails:

  <== match case [a, x <: Foo[?, ?]#A] =>> scala.runtime.MatchCase[Foo[a, x], x] vs Foo[String, ("hello" : String)] = Some(NoType)
<== reduce match type Foo[String, ("hello" : String)] match {   case Foo[a, x] => x } 1497850786 = <notype>

@odersky and/or @smarter does it look to you like Foo[?, ?]#A should resolve as to the arg a somehow in isSubArgs? Or do you think this is something that should somehow happen before, when typing the AppledTypeTree for case Foo[a, x] =>? I've looked at some much code but I can't tell with certainty where error is.

There's almost already something there in isSubArgs: the paramBounds method, but that's for TypeBound arguments, and I don't have that, I have TypeBounds in the info of my pattern-symbol arguments...

[dwijnand]

Hey @odersky, perhaps you can help me out, I've been pouring days into trying to understand how typing works on this code. Given case Foo[a, x] => x as a CaseDef, which happens to be for a match type, but equally with something like case foo: Foo[a, x] => foo.getX: x in a regular match, is there a type representation that can be used for x that can reference the A type parameter of Foo? Currently it's Foo[?, ?]#A (TypeRef(AppliedType)), but that then that doesn't lead to it subtyping.

[odersky]

It's not my field. I think @OlivierBlanvillain is better placed to answer.