Dotty: issue unifying match types when using an opaque type.

[johnynek]

My goal was to make an Lt[N <: Int] type and use it to make a safe get operation from a list. I found I could implement the code, but it wouldn't compile when the List type was itself an opaque type, but would when the List type was the standard library (class based type).

Minimized code

I used 0.23.0-RC1
see: https://gist.github.com/johnynek/de9816f26f2c54c4f33a5890ed0bfab9

Output

[error] -- [E007] Type Mismatch Error: /home/oscarboykin/oss/dotty-example-project/src/main/scala/OList.scala:72:18 
[error] 72 |  val one = list3(0: Lt[3])
[error]    |                  ^^^^^^^^
[error]    |                Found:    (2 : Int) | ((1 : Int) | LtType.Lt[(1 : Int)])
[error]    |                Required: LtType.Lt[N]
[error]    |
[error]    |                where:    N is a type variable with constraint <: Int
[error] one error found
[error] (Compile / compileIncremental) Compilation failed
[error] Total time: 1 s, completed Apr 4, 2020 1:57:13 PM

Expectation

Strangely, when I use a standard (class-based) List, the code compiles (see second linked example). But when the List is itself an opaque type, it fails.

If feels like somehow the features don't compose. It is unclear why using match types with an opaque type should change unification.

[smarter]

There's no working subtyping for match types, I think you're running into that: https://github.com/lampepfl/dotty/issues/8666#issuecomment-609099621

Strangely, when I use a standard (class-based) List, the code compiles (see second linked example).

In your second example, your apply extension method is not called, because List already has an apply method, and you're in the scope where the opaque type is defined so it's not opaque.

[johnynek]

yes, indeed, if I change the extension method to fetch I get the same error in both cases.

I don't see why subtyping is the question. It seems to typecheck (2: Lt[3]) correctly. Somehow it doesn't seem to be unifying SList[3, Int] with a method def [N, A](self: SList[N, A]).fetch(n: Lt[N]) such that N = 3. The error is like N is unknown:

[error] 72 |  val one = list3.fetch(0: Lt[3])
[error]    |                        ^^^^^^^^
[error]    |                Found:    (2 : Int) | ((1 : Int) | LtType.Lt[(1 : Int)])
[error]    |                Required: LtType.Lt[N]
[error]    |
[error]    |                where:    N is a type variable with constraint <: Int

So it isn't clear to me why LtType.Lt[(1: Int)] isn't reduced to (0: Int) and I'm not sure why it isn't saying Required: LtType.Lt[(3: Int)].

Note, another smaller example seems to work:

  import scala.compiletime.S

  type Lt[N <: Int] <: Int =
    N match {    
      case 0 => Nothing
      case 1 => 0
      case S[n] => n | Lt[n]
    }

  def check[N <: Int](lt: Lt[N]): Unit = ()

  // these compile                          
  check[3](2)                              
  check[3](1)                                                          
  check[3](0)   

So, I'm not sure why check can typecheck, but fetch can't.

[johnynek]

interestingly, in the above check example, if I remove the declaration of the type, it does fail:

[error] 61 |  check(3)
[error]    |        ^
[error]    |        Found:    (3 : Int)
[error]    |        Required: LtType.Lt[N]
[error]    |
[error]    |        where:    N is a type variable with constraint <: Int

and it does so with the same kind of error as fetch above. It's like in the fetch example, despite knowing that list3: SList[3, Int] it has forgotten that N = (3: Int) by the time it is typechecking fetch.

[smarter]

t seems to typecheck (2: Lt[3]) correctly.

That's not the issue. The issue is that as far as the type system is concerned, Lt{3] is a type that reduces to 3 | ..., and Lt[N] is a completely unrelated abstract type. There is no logic in the compiler that lets it infer N = 3, this is exactly the same problem as in https://github.com/lampepfl/dotty/issues/8666#issuecomment-609099621.

if I remove the declaration of the type, it does fail:

Yep, if you pass in the type parameter there is no problem, because the compiler doesn't have to solve Lt{3] <:< Lt[N] for some type variable N, since you already gave it the answer N := 3

[bishabosha]

@smarter do you think this is a duplicate issue?

[smarter]

Yes I think it's a dupe of #8666 since the root cause is the same.

[bishabosha]

The issues are linked now anyway