Kinds not conforming with type lambda

Question

Having trouble with type "kinds":

trait Sys[ S <: Sys[S]]
trait Expr[S <: Sys[S], A]
trait Attr[S <: Sys[S], A[_]]
def test[  S <: Sys[S]]: Attr[S, ({type l[x<:Sys[x]]=Expr[x,Int]})#l] = ???

This fails with

error: kinds of the type arguments (S,[x <: Sys[x]]Expr[x,Int]) do not conform
to the expected kinds of the type parameters (type S,type A) in trait Attr.
[x <: Sys[x]]Expr[x,Int]'s type parameters do not match type A's expected parameters:
type x's bounds <: Sys[x] are stricter than type _'s declared bounds >: Nothing <: Any
           def test[S <: Sys[S]]: Attr[S, ({type l[x<:Sys[x]]=Expr[x,Int]})#l] = ???
                                  ^

What's the problem with the declared bounds? Do I need to carry that cr*ppy partially applied type into the type constructor of trait Attr? And why? Can I fix this without touching the definition of Attr?

I do need the bounds in function test in order for the implementation to work, but I do not want to proliferate those bounds to the public interface Attr.

---

Note: If I use a type member (what I don't want), it works:

trait Attr[S <: Sys[S]] { type A[_]}
def test[  S <: Sys[S]]: Attr[S] { type A[S <: Sys[S]] = Expr[S, Int]} = ???

Answer 1

As you observed, you can't always mismatch bounds when providing a higher-kinded type argument. Interestingly, it is actually a variance issue:

class A
class B extends A
trait NeedsNeedsA[T[S <: A]]
trait NeedsNeedsB[T[S <: B]]
trait NeedsA[S <: A]
trait NeedsB[S <: B]

def x: NeedsNeedsA[NeedsB] // fails
def y: NeedsNeedsB[NeedsA] // works

which makes sense if you think of a higher-kinded type as a function on types, contravariant in its argument's bound.

Interestingly, in a structural type, which is on the surface a lot like subtyping, Scala does not give the same error:

def t: MemberNeedsA { type T[S <: B] }
def u: MemberNeedsB { type T[S <: A] }

the reason being that a structural type is sort of like an intersection:

def s: MemberNeedsA with MemberNeedsB

and it may be that that intersection cannot actually exist in nature, but Scala doesn't check that.

OK, but that's not so relevant to your question. Back to your question: I think you have a variance issue. You want test to give the caller back an Attr, and an Attr posseses a type function (A[_]), and you want to say, this Attr has a type function that requires a more specific argument. I think you can see why you shouldn't be allowed to do that -- it's the same reason you can't substitute a function requiring a more specific argument in place of one that would require a more general argument.

At this point I'm afraid the solution will have to depend on what you want Attr to be able to accomplish. You need to figure out why you need to restrict the type argument in some cases more than others. If it makes conceptual sense in your program that "some Attrs are more restrictive than others", you could define:

trait Attr[S <: Sys[S], B[Y <: B[Y]], A[X <: B[X]]]
def test[S <: Sys[S]]: Attr[S, Sys, L] = ...

But the solution will depend on what the restriction on A[_]'s argument is intended to mean.