Subtype check fails as AnyKind type parameter for type functions with different but compatible bounds

[s5bug]

Compiler version

3.3.5
3.6.3
3.6.4-RC1

Minimized code

type A >: X
type B <: Y
type C[x] <: Z[x]

type X
type Y
type Z[x]

type F1[x >: A <: B] = C[x]
type F2[x >: X <: Y] = Z[x]

def `f1 <: f2`[x >: A <: B](f1: F1[x]): F2[x] = f1

class Cov[+F <: AnyKind]
def `cov[f1] <: cov[f2]`(cf1: Cov[F1]): Cov[F2] = cf1

Output

Found:    (cf1 : Playground.Cov[Playground.F1])
Required: Playground.Cov[Playground.F2]

Explanation
===========

Tree: cf1
I tried to show that
  (cf1 : Playground.Cov[Playground.F1])
conforms to
  Playground.Cov[Playground.F2]
but none of the attempts shown below succeeded:

  ==> (cf1 : Playground.Cov[Playground.F1])  <:  Playground.Cov[Playground.F2]
    ==> Playground.F1  <:  Playground.F2
      ==> Playground.F1  <:  [x >: Playground.X <: Playground.Y] =>> Playground.Z[x]
        ==> [x >: Playground.A <: Playground.B] =>> Playground.C[x]  <:  [x >: Playground.X <: Playground.Y] =>> Playground.Z[x]
          ==> type bounds [ >: Playground.X <: Playground.Y]  <:  type bounds [ >: Playground.A <: Playground.B]
            ==> Playground.A  <:  Playground.X
              ==> Any  <:  Playground.X  = false
    ==> Playground.Cov[Playground.F1]  <:  Playground.Cov[Playground.F2]
      ==> Playground.F1  <:  Playground.F2
        ==> Playground.F1  <:  [x >: Playground.X <: Playground.Y] =>> Playground.Z[x]
          ==> [x >: Playground.A <: Playground.B] =>> Playground.C[x]  <:  [x >: Playground.X <: Playground.Y] =>> Playground.Z[x]
            ==> type bounds [ >: Playground.X <: Playground.Y]  <:  type bounds [ >: Playground.A <: Playground.B]
              ==> Playground.A  <:  Playground.X
                ==> Any  <:  Playground.X  = false

The tests were made under the empty constraint

Expectation

The bounds >: A <: B are "tighter" than the bounds >: X <: Y. I would expect the subtyping check for the variance wrapper around the type functions to succeed.

[s5bug]

Oh. I see where I went wrong. [small] =>> ... doesn't widen to [big] =>> ... because otherwise it could be applied to types outside of its range.

[s5bug]

Just to double-check this,

type A <: X
type B >: Y
type C[x] <: Z[x]

type X
type Y
type Z[x]

type F1[x >: A <: B] = C[x]
type F2[x >: X <: Y] = Z[x]

def `f1 <: f2`[x >: X <: Y](f1: F1[x]): F2[x] = f1

class Cov[+F <: AnyKind]
def `cov[f1] <: cov[f2]`(cf1: Cov[F1]): Cov[F2] = cf1

compiles. Whoops...

[s5bug]

@SethTisue Would you possibly be able to also mark as itype:invalid rather than itype:bug?