Subtype checking for path-dependent types ignores singletons (without eta-expansion)

[Blaisorblade]

In the code below, I'd hope for Client(Server0) to be accepted, without the need for eta-expansion. Achieving this appears important in the literature on path-dependent types.

trait MapImpl {
  type Key
  type Value
  type Map
  val lookup: Map => Key => Value
}
import scala.collection.immutable.HashMap

class HashMapImpl[K, V] extends MapImpl {
  type Key = K
  type Value = V
  type Map = HashMap[K, V]
  val lookup: Map => Key => Value = m => k => m(k)
}

object Foo {
  val Server0:
    (mImpl: MapImpl) => mImpl.Map => mImpl.Key => mImpl.Value
    = mImpl => mImpl.lookup
  val Client:
    (server: (mImpl: MapImpl & {type Key = String} & {type Value = Int}) => mImpl.Map => String => Int) => Int =
    server => server(HashMapImpl[String, Int])(HashMap())("test lookup key") //works
    // server => server(??? : (HashMapImpl[String, Int]))(???)("test lookup key") //works
    // server => server(???)(???)("test lookup key") // crashes
  val Server1: (mImpl: MapImpl & {type Key = String} & {type Value = Int}) => mImpl.Map => String => Int =
    mImpl => Server0(mImpl)
  val Result1: Int = Client(Server0) // rejected
  val Result2: Int = Client(Server1) // accepted
  val Result3: Int = Client(mImpl => Server0(mImpl)) // accepted
}

gives:

-- [E007] Type Mismatch Error: /Users/pgiarrusso/git/dotty-example-project/src/main/scala/foo.scala:27:28
27 |  val Result1: Int = Client(Server0) // rejected
   |                            ^^^^^^^
   |Found:    (mImpl: MapImpl) => (mImpl.Map => mImpl.Key => mImpl.Value)(Foo.Server0)
   |Required: (mImpl: MapImpl & Object{Key = String} & Object{Value = Int}) => mImpl.Map =>
   |  String
   | => Int
one error found

BTW, inspecting source code suggests a potential similar problem for methods: matchingMethodParams(tp1, tp2) only performs dependent substitution on tp2, but here we need "dependent substitution" on tp1 as well.

[smarter]

Is this a special case of #6357 ?

[Blaisorblade]

Well, it seems not, but this problem is probably blocked on that one. However, here subtyping checking fails much earlier, because of String != mImpl.Key and Int != mImpl.Value. Here's the -explain-types output:

error] -- [E007] Type Mismatch Error: /Users/pgiarrusso/git/dotty-example-project/src/main/scala/foo.scala:27:28
[error] 27 |  val Result1: Int = Client(Server0) // rejected
[error]    |                            ^^^^^^^
[error]    |Found:    (mImpl: MapImpl) => (mImpl.Map => mImpl.Key => mImpl.Value)(Foo.Server0)
[error]    |Required: (mImpl: MapImpl{Key = String; Value = Int}) => mImpl.Map => String => Int
[error]    |Constraint(
[error]    | uninstVars = ;
[error]    | constrained types =
[error]    | bounds =
[error]    | ordering =
[error]    |)
[error]    |Subtype trace:
[error]    |  ==> (mImpl: MapImpl) => (mImpl.Map => mImpl.Key => mImpl.Value)(Foo.Server0) <:< (mImpl: MapImpl{Key = String; Value = Int}) => mImpl.Map => String => Int
[error]    |    ==> MapImpl => Nothing => Nothing => MapImpl#Value <:< MapImpl{Key = String; Value = Int} => Nothing => String => Int LoApprox
[error]    |      ==> scala.type(scala) <:< scala.type(scala)
[error]    |      <== scala.type(scala) <:< scala.type(scala)   = true
[error]    |      ==> MapImpl{Key = String; Value = Int} <:< MapImpl
[error]    |        ==> MapImpl <:< MapImpl
[error]    |        <== MapImpl <:< MapImpl   = true
[error]    |      <== MapImpl{Key = String; Value = Int} <:< MapImpl   = true
[error]    |      ==> Nothing => Nothing => MapImpl#Value <:< Nothing => String => Int
[error]    |        ==> scala.type(scala) <:< scala.type(scala)
[error]    |        <== scala.type(scala) <:< scala.type(scala)   = true
[error]    |        ==> Nothing <:< Nothing
[error]    |        <== Nothing <:< Nothing   = true
[error]    |        ==> Nothing => MapImpl#Value <:< String => Int
[error]    |          ==> scala.type(scala) <:< scala.type(scala)
[error]    |          <== scala.type(scala) <:< scala.type(scala)   = true
[error]    |          ==> String <:< Nothing
[error]    |          <== String <:< Nothing   = false
[error]    |        <== Nothing => MapImpl#Value <:< String => Int   = false
[error]    |      <== Nothing => Nothing => MapImpl#Value <:< Nothing => String => Int   = false
[error]    |    <== MapImpl => Nothing => Nothing => MapImpl#Value <:< MapImpl{Key = String; Value = Int} => Nothing => String => Int LoApprox  = false
[error]    |  <== (mImpl: MapImpl) => (mImpl.Map => mImpl.Key => mImpl.Value)(Foo.Server0) <:< (mImpl: MapImpl{Key = String; Value = Int}) => mImpl.Map => String => Int   = false
[error] one error found
[error] (Compile / compileIncremental) Compilation failed
[error] Total time: 4 s, completed May 13, 2019 9:50:49 PM

Indeed, MapImpl{Key = String; Value = Int} <:< MapImpl seems to not be a problem. However, the trace of #6357 checks that again later, confusingly. I'm also confused by the answer:

Dependent function types are specified to be refinements of plain function types, which implies they are non-variant in their parameters.

Are refinements invariant? I'm not sure why...

[smarter]

Are refinements invariant? I'm not sure why...

Because they're also used for structural typing which can be translated to reflective calls on the JVM, and there's no built-in variance in the JVM, instead different parameter types correspond to different overloads. I'm exploring using a magic marker trait to work around that limitation for the purpose of encoding functions (all of them: regular, implicit, dependent, polymorphic, ..)

[Blaisorblade]

To be sure, this issue was born out of our other project with you and @sstucki.

For extra fun, this still fails before running into #6357:

  val ServerCast: ((mImpl: MapImpl {type Key = String; type Value = Int}) => mImpl.Map => mImpl.Key => mImpl.Value) = Server0 //fails

Here we get subtype checking to say that mImpl.Key <:< mImpl.Key fails, because it becomes String <:< Nothing (see log below). I suspect we get Nothing because Dotty is normalizing mImpl.Key where mImpl: MapImpl. But it shouldn't — that's the wrong binding for mImpl!

Take DOT's subtyping rule for function types:

Γ ⊢ S₂ <: S₁    Γ, x: S₂ ⊢ T₁ <: T₂
----------------------------------- (T-→-<:-→)
Γ ⊢ (x: S₁) → T₁ <: (x: S₂) → T₂

Here, we check T₁ <: T₂ in a context with x: S₂, which is the more specific type. More concretely, here we need:

Γ ⊢ MapImpl {type Key = String; type Value = Int} <: MapImpl    Γ, x: MapImpl {type Key = String; type Value = Int} ⊢ T₁ <: T₂
----------------------------------- (T-→-<:-→)
Γ ⊢ (x: MapImpl) → T₁ <: (x: MapImpl {type Key = String; type Value = Int}) → T₂

where T₁ = T₂ = mImpl.Map => mImpl.Key => mImpl.Value. However, one mImpl.Key is already typechecked and resolved relative to mImpl.Key.

Hence, implementing this rule correctly might require some additional substitution in Dotty, unlike on paper? That might be why eta-expansion is an effective workaround.

-- [E007] Type Mismatch Error: src/main/scala/foo.scala:35:118 -----------------
35 |  val ServerCast: ((mImpl: MapImpl {type Key = String; type Value = Int}) => mImpl.Map => mImpl.Key => mImpl.Value) = Server0 //fails
   |                                                                                                                      ^^^^^^^
   |Found:    (mImpl: MapImpl) => (mImpl.Map => mImpl.Key => mImpl.Value)(Foo.Server0)
   |Required: (mImpl: MapImpl{Key = String; Value = Int}) => mImpl.Map => mImpl.Key =>
   |  mImpl.Value
   |Constraint(
   | uninstVars = ;
   | constrained types =
   | bounds =
   | ordering =
   |)
   |Subtype trace:
   |  ==> (mImpl: MapImpl) => (mImpl.Map => mImpl.Key => mImpl.Value)(Foo.Server0) <:< (mImpl: MapImpl{Key = String; Value = Int}) => mImpl.Map => mImpl.Key =>
   |  mImpl.Value
   |    ==> MapImpl => Nothing => Nothing => MapImpl#Value <:< MapImpl{Key = String; Value = Int} => Nothing => String => Int LoApprox
   |      ==> scala.type(scala) <:< scala.type(scala)
   |      <== scala.type(scala) <:< scala.type(scala)   = true
   |      ==> MapImpl{Key = String; Value = Int} <:< MapImpl
   |        ==> MapImpl <:< MapImpl
   |        <== MapImpl <:< MapImpl   = true
   |      <== MapImpl{Key = String; Value = Int} <:< MapImpl   = true
   |      ==> Nothing => Nothing => MapImpl#Value <:< Nothing => String => Int
   |        ==> scala.type(scala) <:< scala.type(scala)
   |        <== scala.type(scala) <:< scala.type(scala)   = true
   |        ==> Nothing <:< Nothing
   |        <== Nothing <:< Nothing   = true
   |        ==> Nothing => MapImpl#Value <:< String => Int
   |          ==> scala.type(scala) <:< scala.type(scala)
   |          <== scala.type(scala) <:< scala.type(scala)   = true
   |          ==> String <:< Nothing
   |          <== String <:< Nothing   = false
   |        <== Nothing => MapImpl#Value <:< String => Int   = false
   |      <== Nothing => Nothing => MapImpl#Value <:< Nothing => String => Int   = false
   |    <== MapImpl => Nothing => Nothing => MapImpl#Value <:< MapImpl{Key = String; Value = Int} => Nothing => String => Int LoApprox  = false
   |  <== (mImpl: MapImpl) => (mImpl.Map => mImpl.Key => mImpl.Value)(Foo.Server0) <:< (mImpl: MapImpl{Key = String; Value = Int}) => mImpl.Map => mImpl.Key =>
   |  mImpl.Value   = false
one error found

To get #6357, one must workaround all those bugs by using fewer dependent types, and then we get it with:

  val foo0 : (mImpl: MapImpl) => String => Int = ???
  val foo1 : (mImpl: MapImpl {type Key = String; type Value = Int}) => String => Int = foo0 //fails due to #6357.`
``