scala / scala3

The Scala 3 compiler, also known as Dotty.
https://dotty.epfl.ch
Apache License 2.0
5.86k stars 1.06k forks source link

BitSet does not conform to Set[Int] in match type #14593

Closed Adam-Vandervorst closed 2 years ago

Adam-Vandervorst commented 2 years ago

Compiler version

3.1.3-RC1-bin-20220228-fa08d00-NIGHTLY

Minimized code

import scala.collection.immutable.BitSet

type SetFor[A] <: Set[A] = A match
  case Int => BitSet
  case A => Set[A]

Output

  case Int => BitSet
              ^^^^^^
              Found:    collection.BitSet
              Required: Set[A]

Expectation

Compile and match correctly.

dwijnand commented 2 years ago

I assume there was just an error in reproduction or minimisation and you meant scala.collection.immutable.BitSet, as in:

import scala.collection.immutable.BitSet

type SetFor[A] <: Set[A] = A match
  case Int => BitSet
  case A => Set[A]

Here's the -explain output:

-- [E007] Type Mismatch Error: tests/pos/i14593.scala:2:41 -----------------------------------------------------------------------
2 |  case Int => scala.collection.immutable.BitSet
  |              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  |              Found:    collection.immutable.BitSet
  |              Required: Set[A]
  |-------------------------------------------------------------------------------------------------------------------------------
  | Explanation (enabled by `-explain`)
  |- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
  |
  | Tree: scala.collection.immutable.BitSet
  | I tried to show that
  |   collection.immutable.BitSet
  | conforms to
  |   Set[A]
  | but the comparison trace ended with `false`:
  |
  |   ==> collection.immutable.BitSet  <:  Set[A]
  |     ==> Set[Int]  <:  Set[A] (left is approximated)
  |       ==> (scala.collection.immutable : scala.collection.immutable.type)  <:  collection.immutable.type
  |       <== (scala.collection.immutable : scala.collection.immutable.type)  <:  collection.immutable.type = true
  |       ==> A  <:  Int
  |         ==> Any  <:  Int (left is approximated)
  |         <== Any  <:  Int (left is approximated) = false
  |       <== A  <:  Int = false
  |     <== Set[Int]  <:  Set[A] (left is approximated) = false
  |   <== collection.immutable.BitSet  <:  Set[A] = false
  |
  | The tests were made under the empty constraint
   -------------------------------------------------------------------------------------------------------------------------------

So looks like when A is matched with Int, A := Int (or perhaps A =:= Int) isn't added to the constraints such that this is true.

smarter commented 2 years ago

A := Int

I don't think that's true, at best you know that A <: Int, so Set[Int] and Set[A] are unrelated.

dwijnand commented 2 years ago

A := Int

I don't think that's true, at best you know that A <: Int, so Set[Int] and Set[A] are unrelated.

Ah, yes, of course. Got confused by Set's immutability and Int's finality. But that doesn't impede A being some subtype, like 1. Here's an equivalent term version that also fails for this same version:

scala> def mk[A <: Int]: Set[A] = new scala.collection.immutable.BitSet
-- [E007] Type Mismatch Error: -------------------------------------------------
1 |def mk[A <: Int]: Set[A] = new scala.collection.immutable.BitSet
  |                           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  |                     Found:    scala.collection.immutable.BitSet
  |                     Required: Set[A]
  |
  |                     where:    A is a type in method mk with bounds <: Int
  |-----------------------------------------------------------------------------
  | Explanation (enabled by `-explain`)
  |- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
  |
  | Tree: new scala.collection.immutable.BitSet()
  | I tried to show that
  |   scala.collection.immutable.BitSet
  | conforms to
  |   Set[A]
  | but the comparison trace ended with `false`:
  |
  |   ==> scala.collection.immutable.BitSet  <:  Set[A]
  |     ==> Set[Int]  <:  Set[A] (left is approximated)
  |       ==> A  <:  Int
  |         ==> Int  <:  Int (left is approximated)
  |           ==> scala.type  <:  (scala : scala.type)
  |           <== scala.type  <:  (scala : scala.type) = true
  |         <== Int  <:  Int (left is approximated) = true
  |       <== A  <:  Int = true
  |       ==> Int  <:  A
  |         ==> Int  <:  Nothing in frozen constraint
  |         <== Int  <:  Nothing in frozen constraint = false
  |       <== Int  <:  A = false
  |     <== Set[Int]  <:  Set[A] (left is approximated) = false
  |   <== scala.collection.immutable.BitSet  <:  Set[A] = false
  |
  | The tests were made under the empty constraint
   -----------------------------------------------------------------------------
1 error found
Adam-Vandervorst commented 2 years ago

I'm sorry, I don't see why that argument holds up on the type level level constructs (that is, why this code would be analogous to the value-level code of @dwijnand). Say one allowed this match type, what would go wrong?

As a side-note, this seemed to me like a perfect use-case match-types, and the docs show something remarkably similar. What pattern would allow for this specialization?

Adam-Vandervorst commented 2 years ago

My underlying assumption was that match types would only match whatever you specified in the case like with normal match case statements. I'm new to using these, but intuitively case Int => would only match exactly Int. While case i: Int or case i <: Int would match anything conforming to Int.

smarter commented 2 years ago

intuitively case Int => would only match exactly Int

That's not how it's specified, see http://dotty.epfl.ch/docs/reference/new-types/match-types.html :

Match type reduction follows the semantics of match expressions, that is, a match type of the form S match { P1 => T1 ... Pn => Tn } reduces to Ti if and only if s: S match { : P1 => T1 ... : Pn => Tn } evaluates to a value of type Ti for all s: S.

This behavior allows for typing a match expression with a match type (see section "Dependent Typing").

Adam-Vandervorst commented 2 years ago

Ha, really "match types" (the types a match expression would have) and not "type matches" (match expressions for types).

Is there any way to do this than? Because, since types work the same in macros, this wouldn't work for the TreeSet/HashSet example either (despite having the same use-case).

smarter commented 2 years ago

Your original example would work without an upper bound (type SetFor[A] = A match ...), if you always pass a concrete type that could be good enough.

Adam-Vandervorst commented 2 years ago

Well without the bound I (understandably) get errors like

value | is not a member of SetFor[A]

when trying to apply set union on two specialized sets.

smarter commented 2 years ago

But if you're trying to be generic over the kind of Set you're operating, why not use Set[A] directly? It's only when creating some collection that you need to care about what Set you're using.

Adam-Vandervorst commented 2 years ago

I don't think that's possible in my case, but I'd love to be proven wrong:

transparent inline def evidenceLattice[A]: AtomicJoinLattice[(SpecializeSet[A], SpecializeSet[A])] =
  val base = summonInline[Empty[SpecializeSet[A]]].value
  new AtomicJoinLattice[(SpecializeSet[A], SpecializeSet[A])]:
    extension (x: (SpecializeSet[A], SpecializeSet[A]))
      def \/(y: (SpecializeSet[A], SpecializeSet[A])) = (x._1 | y._1, x._2 | y._2)
      def isAtom = x._1.size + x._2.size == 1
    val bottom = (base, base)

which is used in places where BitSet needs to be known

    ImplicitWalker.forone(TestLattice[AtomicJoinLattice, (BitSet, BitSet)]("Counting evidence", evidenceLattice[Int], {
      val range = BitSet.fromSpecific(0 to N).subsets.toVector
      range.flatMap(x => range.map(y => (x, y)))
    }))

and as you probably guessed, this grows like (2^N)^2, making it prohibitively expensive without BitSet.

dwijnand commented 2 years ago

Btw, I also tried to find something that works and failed, and can't tell exactly why it fails while LeafElem and leafElem work. Perhaps it's some solace. 🙂 I'm not never sure where match type questions are being asked and answered...

smarter commented 2 years ago

Maybe something like def evidenceLattice[F[X] <: Set[X] & SetOps[X, F, F[X]], A]: AtomicJoinLattice[(F[A], F[A])] =, but this whole discussion beyond elsewhere, either in https://github.com/lampepfl/dotty/discussions or https://users.scala-lang.org