Type mismatch where 'found' and 'required' coincide.

[scabug]

The following code produces

type mismatch;  found   : candidateUpperObject.result.Lower
                required: candidateUpperObject.result.Lower
where val candidateUpperObject: CanonicalGeneration.this.Upper

I tried adding -uniqid and -explaintypes, and then get

type mismatch;  found   : candidateUpperObject#44447.result#44239.Lower#44231
                required: candidateUpperObject.result#44239.Lower#44231
where val candidateUpperObject: CanonicalGeneration#9908.this.Upper#44230

which doesn't add much to my understanding.

Here's the code; I'm sure it can be reduced slightly.

trait EquivalenceClass[X] {
  def representative: X
  def contains(x: X): Boolean
}

trait Group[G] {
  trait Action[X] {
    def orbits: Set[EquivalenceClass[X]]
    def leastOrbit[B: Ordering](invariant: X => B): EquivalenceClass[X]
  }
}

trait CanonicalGeneration[A <: CanonicalGeneration[A, G, B], G, B] {
  val automorphisms: Group[G]

  implicit val ordering: Ordering[B]
  def invariant: B

  trait Upper {
    val result: A
    def inverse: result.Lower
  }
  trait Lower {
    val result: A
  }

  def upperObjects: automorphisms.Action[Upper]
  def lowerObjects: automorphisms.Action[Lower]

    def children = {
    for (
      orbit <- upperObjects.orbits;
      candidateUpperObject = orbit.representative;
      canonicalReductionOrbit = candidateUpperObject.result.lowerObjects.leastOrbit({ l: candidateUpperObject.result.Lower => l.result.invariant });
      // This next line causes a (spurious?) type mismatch:
      if canonicalReductionOrbit.contains(candidateUpperObject.inverse)
    ) yield candidateUpperObject.result
  }
}

I'm reporting this as a bug on the presumption that when the types shown in after 'found' and 'required' print the same, it's at least a problem with error reporting, if not an actual type checker bug.

[scabug]

Imported From: https://issues.scala-lang.org/browse/SI-6522?orig=1
Reporter: Scott Morrison (scott)
Affected Versions: 2.9.2, 2.10.0-M7

[scabug]

@paulp said:
Your presumption (found == required implies bug) is correct.

[scabug]

@paulp said:
However, and I couldn't tell it from your presentation because there seems to be a newline I don't have, found doesn't == require.

./a.scala:39: error: type mismatch;
 found   : candidateUpperObject.result.Lower
 required: candidateUpperObject.result.Lower where val candidateUpperObject: CanonicalGeneration.this.Upper
      if canonicalReductionOrbit.contains(candidateUpperObject.inverse)
                                                               ^
one error found

The required type is an existential with a clause involving candidateUpperObject, and the found isn't.

[scabug]

Scott Morrison (scott) said:
I'm still confused about this, although happy to close the issue and move to a mailing list if appropriate.

Shouldn't both the types here (required and found) be the path dependent type candidateUpperObject.result.Lower? How did the existential type get involved?

[scabug]

@paulp said:
I don't know; I didn't mean to suggest there's no bug here. The existential type looks malformed - there's no bound on the clause, just the val. I don't have the spare brainpower right now to convince myself they should be the same type, but I can believe it. If the code can be simplified at all, it wouldn't hurt.

[scabug]

Scott Morrison (scott) said:
Here's a significantly reduced case:

trait Z { 
  trait Lower
  trait Upper {
    val result: Z
    def inverse: result.Lower
  }

  def upperObject: Upper
  def lowerPredicate: Lower => Boolean

  def thisOneWorks = {
    val upper = upperObject
    val predicate = upper.result.lowerPredicate
    predicate(upper.inverse)
  }
  
  def butThisOneDoesnt = {
    for (
      upper <- Seq(upperObject);
      predicate = upper.result.lowerPredicate
    ) yield predicate(upper.inverse)
  }
}

The error is now

type mismatch;
 found   : upper.result.Lower
 required: upper.result.Lower where val upper: Z.this.Upper

on the predicate(upper.inverse) call in butThisOneDoesnt. I included a slight variation under thisOneWorks because it looks like the for-loop syntax is somehow involved.

[scabug]

@paulp said (edited on Oct 18, 2012 3:16:44 AM UTC):
Here it is reformulated for contrast. The "def nok" version is the moral equivalent of yours, the one which doesn't compile. All the others do. I believe this falls somewhere between limitation and bug.

trait Z {
  trait Lower
  trait Upper {
    val result: Z
    def inverse: result.Lower
  }

  val upper: Upper
  val pred: Lower => Unit

  def ok1 = Seq(upper) map { u => u.result.pred(u.inverse) }
  def ok2 = Seq(upper) map { u =>              u.result.pred match { case p               => p(u.inverse) } }
  def ok3 = Seq(upper) map { u =>                  u.inverse match { case x               => u.result.pred(x) } }
  def ok4 = Seq(upper) map { u => (u.result.pred, u.inverse) match { case (p, x)          => p(x) } }
  def ok5 = Seq(upper) map { u => (u.result.pred, u        ) match { case (p, u1: u.type) => p(u1.inverse) } }
  def nok = Seq(upper) map { u => (u.result.pred, u        ) match { case (p, u1)         => p(u1.inverse) } }

  /**

  a.scala:15: error: type mismatch;
   found   : u1.result.Lower
   required: u.result.Lower
    def nok = Seq(upper) map { u => (u.result.pred, u) match { case (p, u1) => p(u1.inverse) } }
                                                                                    ^
  **/
}

[scabug]

@paulp said:
In the for comprehension version, the intermediate value I called u1 is hidden from sight, so there's no way, at least no obvious way, to type ascript it to preserve the singleton type of u. And so it gets lost.

[scabug]

Scott Morrison (scott) said:
Thanks Paul, that's very clear now!

[scabug]

@paulp said:
Through an accident of timing, I noticed this is a direct consequence of #837.