Constraint resolution failing for match type argument

[nicolasstucki]

class Foo {

  type E[X]

  def i: Int = ???
  def e: E[Int] = ???

  // Transforms `(T1, ... Tn)` into `(E[T1], ..., E[Tn])`
  type F[T <: Tuple] <: Tuple = T match {
    case Unit => Unit
    case h *: t => E[h] *: F[t]
  }

  def foo1[Args <: Tuple](args: Args, args2: F[Args]): Unit = ()

  foo1((i, i), (e, e)) // fails
  foo1((i, i), (e, e): F[(Int, Int)]) // fails

}

fails with

-- [E007] Type Mismatch Error: Foo.scala:16:15 ---------------------------------
16 |  foo1((i, i), (e, e)) // fails
   |               ^^^^^^
   |Found:    (Foo.this.E[Int], Foo.this.E[Int])
   |Required: Foo.this.F[Args]
   |
   |where:    Args is a type variable with constraint >: (Int, Int) and <: Tuple
-- [E007] Type Mismatch Error: Foo.scala:17:15 ---------------------------------
17 |  foo1((i, i), (e, e): F[(Int, Int)]) // fails
   |               ^^^^^^^^^^^^^^^^^^^^^
   |Found:    Foo.this.E[Int] *: Foo.this.E[Int] *: Foo.this.F[Unit]
   |Required: Foo.this.F[Args]
   |
   |where:    Args is a type variable with constraint >: (Int, Int) and <: Tuple

where Args should be inferred as (Int, Int).

[nicolasstucki]

Same happens for

class Foo {

  type E[X]

  def i: Int = ???
  def e: E[Int] = ???

  // Transforms `(T1, ... Tn)` into `(E[T1], ..., E[Tn])`
  type F[T <: Tuple] <: Tuple = T match {
    case Unit => Unit
    case h *: t => E[h] *: F[t]
  }

  def foo2[Args <: Tuple, Args2 >: F[Args] <: F[Args]](args: Args, args2: Args2): Unit = ()

  foo2((i, i), (e, e)) // fails

  // all these work
  foo2[(Int, Int), F[(Int, Int)]]((i, i), (e, e))
  foo2[(Int, Int), F[(Int, Int)]]((i, i), (e, e))
  foo2[(Int, Int), F[Int *: Int *: Unit]]((i, i), (e, e))
  foo2[(Int, Int), (E[Int], E[Int])]((i, i), (e, e))
  foo2[(Int, Int), E[Int] *: E[Int] *: Unit]((i, i), (e, e))

}

which fails with

-- [E007] Type Mismatch Error: Foo.scala:16:15 ---------------------------------
16 |  foo2((i, i), (e, e)) // fails
   |               ^^^^^^
   |Found:    (Foo.this.E[Int], Foo.this.E[Int])
   |Required: Foo.this.F[Args]
   |
   |where:    Args is a type variable with constraint >: (Int, Int) and <: Tuple

[odersky]

These are problems of type inference, since the argument to the match type is not instantiated at the point where the typecheck is made. For comparison, this works:

  foo1[(Int, Int)]((i, i), (e, e))

On the other hand, this does not work either:

  def foo2[Args <: Tuple](args: Args)(args2: F[Args]): Unit = ()
  foo2(i, i)(e, e) // fails

One would hope that the first application to (i, i) instantiates Args so that the second application can pass. But that's not the case. Args is only instantiated on demand, and we do not recognize the demand here.

[milessabin]

I have something very similar working very nicely here,

type LiftP[F[_], T] <: Tuple = T match {
  case Unit => Unit
  case a *: b => F[a] *: LiftP[F, b]
}

As far as I can see the only difference is that in this case the applied type constructor is a parameter whereas in your case it's closed over?

Parenthetically, I'd like to recommend dropping redundant argument bounds like <: Tuple ... they're very noisy and propagate all the way through the call chain. IMO that outweighs any advantages they might have in terms of improved error messages.

[odersky]

It looks difficult to me how improve on the status quo here.

[odersky]

This seems to work now.