What does 'do not conform to trait Builder's type parameter bounds' mean in scala?

Question

I have the following simple program that defines 2 identical upper bounds for type parameter and abstract type alias respectively:

package scala.spike.typeBoundInference

object Example1 {
  trait Domain {
  }

  trait Impl {

    type DD <: Domain
    type GG <: StaticGraph[DD]

    type A1
    type A2
    type A3
    // ... this type list can go very long
    // so inlining them as generic type parameters is impossible


    final type Builder = StaticGraph.Builder[DD, GG]
  }

  trait DSL[I <: Impl] {

    val impl: StaticGraph.Builder[I#DD, I#GG]
  }

  trait StaticGraph[T <: Domain] {}

  object StaticGraph {

    trait Builder[D <: Domain, G <: StaticGraph[D]] {}

  }
}

However, scala refuse to compile it:

Error:(16, 27) type arguments [I#DD,I#GG] do not conform to trait Builder's type parameter bounds [D <: scala.spike.typeBoundInference.Example1.Domain,G <: scala.spike.typeBoundInference.Example1.StaticGraph[D]] val impl: StaticGraph.Builder[I#DD, I#GG]

What could possibly go wrong here?

• DD <: Domain check

• GG <: StaticGraph[DD] check

there is no reason scala think it is unsafe.

In the meantime, I found that if class StaticGraph[T] is declared as covariant scala compiler will run successfully. This is even worse (for some reason StaticGraph[T] has to be invariant), as type bound GG <: StaticGraph[DD] means that if type DD is determined, then GG is a subclass of StaticGraph[DD], but not necessary a subclass of StaticGraph[Domain], which is exactly what I want here.

UPDATE 1: I've read all the answers and comments and somehow got the impression that the core reason is that there is no guarantee that for any instance i of Impl, the type bound only guarantee that type

i.DD <:< Impl#DD and Imp#GG <:< StaticGraph[Impl#DD]

but not StaticGraph[i.DD] <:< StaticGraph[Impl#GG]

thus i.GG <:< StaticGraph[i.DD] is also not guaranteed.

However, I've done a quick experiment to verify this idea, which turns out to be not ture:

object Example1 {

  trait Domain {}
  class D1 extends Domain {}

  trait Impl {

    type DD <: Domain
    type GG <: StaticGraph[DD]
  }

  class StaticGraph[T <: Domain] {}

  object Impl1 extends Impl {

    type DD = D1
    type GG = StaticGraph[Domain]
  }

  //or this:

  val impl = new Impl {

    type DD = D1
    type GG = StaticGraph[Domain]
  }
}

In this case compiler throw an error:

Error:(19, 10) overriding type GG in trait Impl with bounds <: scala.spike.TypeBoundInference.Example1.StaticGraph[scala.spike.TypeBoundInference.Example1.Impl1.DD]; type GG has incompatible type type GG = StaticGraph[Domain]

If you think the type constraint doesn't hold for some instances, could you give me counter example?

UPDATE2: turns out that according to the answer, this is true:

i.GG <:< StaticGraph[i.DD]

but this maybe false:

Impl#GG <:< StaticGraph[Impl#GG].

so in the context of DSL this may also be false:

I#GG <:< StaticGraph[I#GG] (3)

But this is only part of the puzzle, to prove that it is type unsafe, we have to construct a counter example of DSL[I] that invalidates condition (3). So the old question remains: is it possible to construct a counter example?

Raze

Shorter example: trait StaticGraph[T]; trait Impl { type DD; type GG <: StaticGraph[DD] }; def f[I <: Impl]: Unit = { implicitly[I#GG <:< StaticGraph[I#DD]] } – Paralipomena

Nice! your example is much better, as the error information directly shows the irony: Error:(12, 40) Cannot prove that I#GG <:< scala.spike.TypeBoundInference.Example3.StaticGraph[I#DD] – Raze

Why don't you use I#Builder instead?, it works for me. – Kiloliter

@LuisMiguelMejíaSuárez yeah it is a valid bypass, but they are the same thing, so theoretically I don't have to do it. – Raze

They aren't the same thing: I#Builder is (approximately) StaticGraph.Builder[i.DD, i.GG] forSome { val i: I }, and StaticGraph.Builder[I#DD, I#GG] is StaticGraph.Builder[i1.DD forSome { val i1: I }, i2.GG forSome { val i2: I} ]. – Bouilli

If you don't want to define Builder in Impl and use I#Builder, you can write val impl: StaticGraph.Builder[i.DD, i.GG] forSome { val i: I } explicitly and that works too. – Bouilli

For update: it's the other way around. i.GG <:< StaticGraph[i.DD] is guaranteed, Impl#GG <:< StaticGraph[Impl#DD] is not. The error is because you need either type DD = Domain or type GG = StaticGraph[D1]. – Bouilli

I got your point, thanks a lot! Will add it as an update. – Raze

Answer 1

OK Problem solved:

import scala.language.higherKinds

object Example5 {

  trait Domain {}
  trait D1 extends Domain

  trait Impl {

    type DD <: Domain
    type GG[T <: Domain] <: StaticGraph[T]
  }

  trait DSL[I <: Impl] {

    val impl: Builder[I#DD, I#GG]
  }

  trait StaticGraph[T <: Domain] {}

  trait Builder[D <: Domain, G[T <: Domain] <: StaticGraph[T]] {}
}

I can't believe I have to use higher kind for such banal matter :-<

Why it compiles? It decouples type constraint and delay it until it becomes necessary. (this is the only explanation I can think of)

Raze

Answer 2

What could possibly go wrong here?

GG <: StaticGraph[DD] check

By declaring type GG <: StaticGraph[DD] you establish a relationship between member types (it's the same as <: StaticGraph[this.DD]). This means that you need to consider instances of Impl.

For any val i: Impl, you have i.DD <: Domain and i.GG <: StaticGraph[i.DD]. You also have i.DD <: I#DD. But you don't have i.DD =:= I#DD! So StaticGraph[i.DD] and StaticGraph[I#DD] are not related (for invariant StaticGraph). And so neither are i.GG (or I#GG) and StaticGraph[I#DD].

To make it compile, you need to require that all i.DD are the same (which also guarantee i.DD =:= I#DD). And there is a way to do that:

trait DSL[T <: Domain, I <: Impl { type DD = T } ] 

will make the code compile (without any other changes).

If StaticGraph is covariant, the relationships work out:

I#GG =:= (kind of)
i.GG forSome { val i: I } <:
StaticGraph[i.DD] forSome { val i: I } <:
StaticGraph[I#DD] forSome { val i: I } =:=
StaticGraph[I#DD]

Bouilli

Sorry, what is "kind of"? I found your initial prose-explanation clearer. Now I'm confused. And what's with those <:? Should they be <:<? – Paralipomena

@AndreyTyukin They are not exactly the same (according to =:=) but they have the same values. implicitly[I#GG =:= i.GG forSome { val i: I }] actually results in Cannot prove that I#GG =:= I#GG. – Bouilli

Oh, those fantastic "cannot prove X =:= X` error messages again. This somehow vaguely reminds me of this strange compiler behavior that you discovered ~11 months ago, you seem to have some kind of special sense for finding those strange examples :) – Paralipomena

The <: is correct (because it's the relation between types), the problem is that there's no corresponding notation for =:= :) – Bouilli

@AndreyTyukin I edited a bit to restore the prose explanation for the invariant case (though SO lost the original revision). Do you think this is better? – Bouilli

@AlexeyRomanov the problem is that in my code i is never instantiated, and there is no such thing referred as StaticGraph[i.DD] (Impl is intend to be only used to reduce the number of generic type parameters, the only possible concrete instance is for DSL), if it exists I have no problem reading the error – Raze

@AlexeyRomanov in addition, the i have 2 ways to inherit type DD: i.DD can be a nested class (which caused the lack of relationship you mentioned), or it can continue to be a type alias (which has no such effect). Regardless, is there a short solution to silence the compiler? – Raze

@AlexeyRomanov, also, may I ask a favour to post the complete scala code for type constraint check? For beginners it is hard to speculate what is happening without actually compiling it. – Raze

@Raze 1. Not instantiating Impl doesn't change what it means. type GG <: StaticGraph[DD] makes a constraint on member types, and doesn't (directly) say anything about projection types I#GG/I#DD at all. In the covariant case, the compiler can prove projection types are related using the relationship on member types; in the invariant case, it can't. – Bouilli

@Raze 2. You are missing an important case: it can not be implemented at all. E.g. it isn't for Impl itself, which is a valid type argument for DSL. Because the definition of DSL doesn't work for this case (Impl#DD is not a subtype of StaticGraph[Impl#GG]), it doesn't work in general, so the compiler doesn't let it through. – Bouilli

@Raze I've extended the answer and added another change which would make your code correct. – Bouilli

Saw your update, thanks a lot! I agree that 'But you don't have i.DD =:= I#DD'. But that solution is impractical, in real case DSL need to refer to scores of member types, which can easily blow up the cap for generic type parameters – Raze

To sum up: path-dependent types are already not too obvious, and type projections are worse. You'll likely be better off adding an instance of I and using path-dependent types directly, but I can't guarantee that without knowing your DSL in more detail. – Bouilli

@AlexeyRomanov obviously I only have 2 options here: either use type projections or use a long list (> 30) of generic type parameters, both are impossible, this means the type system is broken and should be completely avoided. – Raze