Regression in getkyo/kyo for match types / type inference

[WojciechMazur]

Based on OpenCB failure in getkyo/kyo

Compiler version

Last good release: 3.6.4-RC1-bin-20241205-c61897d-NIGHTLY
First bad release: 3.6.4-RC1-bin-20241209-1775d0b-NIGHTLY
Affects 3.6.4-RC1
Bisect points to 2f6e60d

Minimized code

opaque type Tag[A] = String

object Record:
  final class ~[Name <: String, Value] private ()
  opaque type AsField[Name <: String, Value] = Field[Name, Value]
  case class Field[Name <: String, Value](name: Name, tag: Tag[Value])

  object AsField:
    def toField[Name <: String, Value](as: AsField[Name, Value]): Field[?, ?] = as

  object AsFieldsInternal:
    private type HasAsField[Field] = Field match
      case Record.~[name, value] => AsField[name, value]

    inline def summonAsField[Fields](using ev: TypeIntersection[Fields]): Set[Field[?, ?]] =
      TypeIntersection.summonAll[Fields, HasAsField].map(Record.AsField.toField).toSet

sealed abstract class TypeIntersection[A]:
  type AsTuple <: Tuple

object TypeIntersection:
  transparent inline def summonAll[A: TypeIntersection, F[_]]: List[F[Any]] = ???

Output

-- [E007] Type Mismatch Error: /Users/wmazur/projects/scala/community-build3/test.scala:18:59 -----------------------------------------------------------------------------------------------
18 |        TypeIntersection.summonAll[Fields, HasAsField].map(Record.AsField.toField).toSet
   |                                                           ^
   |                                                           Found:    (as : Record.AsFieldsInternal.HasAsField[Any])
   |                                                           Required: Record.AsField[Name, Value]
   |
   |                                                           where:    Name  is a type variable with constraint <: String
   |                                                                     Value is a type variable
   |

Expectation

Should probably compile

[SethTisue]

fyi @fwbrasil

[Gedochao]

cc @dwijnand

[fwbrasil]

If I'm not mistaken we had to introduce AsFieldsInternal to work around another issue. It might be related to #22370. cc/ @road21

[dwijnand]

I'm not sure this is a bug. The same code before #19761 wouldn't have compiled (that I could find) and there's nothing wrong about the avoidance. The reason it widens all the way to Any is because of isUnreducibleWild, because

//     *  Applications of higher-kinded type constructors to wildcard arguments
//     *  are equivalent to existential types, which are not supported.

Any ideas, @sjrd @smarter @odersky ?

[sjrd]

The transparent inline def that returns ??? is probably minimized too much and causing other issues.

[WojciechMazur]

The transparent inline def that returns ??? is probably minimized too much and causing other issues.

Here's original implementation: https://github.com/getkyo/kyo/blob/c060b4164b24868beaa05b6d01078c6b8b1d3f88/kyo-data/shared/src/main/scala/kyo/internal/TypeIntersection.scala#L68-L85

That's also what I initially thought, but the results were the same either if rhs was only ??? or calling an Inliner[R] returning List[R]

[road21]

I have minimized it to

//> using scala 3.6.4-RC1-bin-20241209-1775d0b-NIGHTLY

case class Field[Name](name: Name)
opaque type AsField[Name] = Field[Name] // is compiling without opaque

def toField[Name](as: AsField[Name]): Unit = ()

type HasAsField[f] /*<: AsField[?]*/ = // is compiling with bound
  f match
    case Field[name] => AsField[name]

def x: List[HasAsField[Any]] = ???
x.map(toField)
/* compiler error:
 Found:    (as : tagadt$_.this.HasAsField[Any])
[error] Required: tagadt$_.this.AsField[Name]
 */

def y: HasAsField[Any] = ???
toField(y) // is not compiling even with upper bound

Upper type bound also fixes the original issue in this particular case.

[dwijnand]

Yeah AsField[?] is the isUnreducibleWild that we don't go for in type avoidance. But the example compiles with it manually though. So I think we can close this.

[dwijnand]

I wonder if we should make isUnreducibleWild see if all the wildcard arguments end up as arguments of a class type constructor (like AsField), thus eliminating them as invalid.

[sjrd]

I'm pretty sure that's what it does. But here it's hidden behind an opaque barrier.

[dwijnand]

My point is, given an opaque type alias, applied to wildcard args, where all args end up as args of a class type constructor, is that one of those dangerous akin-to-an-existential that we're trying to protect against? Because if it's not, then perhaps we can allow things like AsField.

[odersky]

My point is, given an opaque type alias, applied to wildcard args, where all args end up as args of a class type constructor, is that one of those dangerous akin-to-an-existential that we're trying to protect against? Because if it's not, then perhaps we can allow things like AsField.

I think it is. You can't find a non-existential form for this which does not reveal the opaque type alias, which is also not allowed.

[dwijnand]

Surely it's allowed within the compiler's calculations? I'm not suggesting we dealias away the opaque type, i.e. return Field[?].

I guess I don't understand the existential types problem. I thought it was similar or related to the bad type bounds can lead to unsoundness, but here I don't understand how the opaqueness of AsField can lead to unsoundness.

I feel like match aliases are in a similar spot, and there we're swinging all the way the other way and just exempting them - && !isMatchAlias - which I presume can lead to unsoundness.

Oh, and btw I checked and type HasAsField[f] <: AsField[?] = ... only compiles because we're not checking that upper bound for isUnreducibleWild ☹

[odersky]

The thing is we don't have a theory for existential types in the Scala context. We don't know how they should behave. So we have to reduce a seemingly existential type to something we do know how to reason about. And we can't in this case.

[SethTisue]

we talked about this a bit at core meeting and somebody was supposed to comment here with further details... but I don't remember who... was it @sjrd?

[dwijnand]

I think we should close this (as mentioned before).

[sjrd]

Ah yes, me.

So yes, after discussion, we consider this a progression. Previously, the type checker was inferring an unsound bound for the match type. That unsound bound leaked a type variable outside of its defining scope, namely <: AsField[name, value], so it was really really bad. Now, it infers something safer, which is sound, but does not allow the rest of the code to typecheck. This is better than what was happening before, although it is annoying in this particular case.

For this case, though, the solution today is to explicitly annotate the desired bound, which is <: AsField[?, ?]. That also allows the rest of the code to typecheck, and it doesn't leak a type variable outside of its defining scope. So use that today as a fix for this particular issue.

Eventually, though, we expect that we will have to rule out wildcard arguments to opaque type aliases altogether, because they're also basically unsound (although it's less obvious than a type variable escaping its scope). So AsField[?, ?] wouldn't be a valid type at all. We'll cross that bridge when we get there.

[fwbrasil]

Thank you everyone for working on this regression. @sjrd I'm attempting to upgrade to 3.6.4 and tried to add the <: AsField[?, ?] bound but I still get a compilation error. Could you clarify where it should be introduced? I'd be happy to restructure the code if needed as well. This transformation could probably be a macro for example.

private type HasAsField[Field] <: AsField[?, ?] =
        Field match
            case name ~ value => AsField[name, value]

    inline def summonAsField[Fields](using ev: TypeIntersection[Fields]): Set[Field[?, ?]] =
        TypeIntersection.summonAll[Fields, HasAsField].map(Record.AsField.toField).toSet

[error] -- [E007] Type Mismatch Error: /Users/fwbrasil/workspace/kyo/kyo-data/shared/src/main/scala/kyo/Record.scala:302:59
[error] 302 |        TypeIntersection.summonAll[Fields, HasAsField].map(Record.AsField.toField).toSet
[error]     |                                                           ^
[error]     |          Found:    (as : kyo.AsFieldsInternal.HasAsField[Any])
[error]     |          Required: kyo.Record.AsField[Name, Value]
[error]     |
[error]     |          where:    Name  is a type variable with constraint <: String
[error]     |                    Value is a type variable
[error]     |
[error]     | longer explanation available when compiling with `-explain`
[error] one error found
[error] (Compile / compileIncremental) Compilation failed

[fwbrasil]

@road21 already fixed it on our side. Thank you! getkyo/kyo#1091