Error proving override check

[MikaelMayer]

Dafny version

latest-nightly

Code to produce this issue

trait ProblemHolder<T(!new, ==)> {
  ghost function Solution(): T

  predicate Problem(solution: T)
    ensures Solution() == solution
}

trait Instantiation extends ProblemHolder<int> {
  ghost function Solution(): int

  predicate Problem(solution: int)
    ensures Solution() == solution
}

Command to run and resulting output

Dafny verify or paste in VSCode

What happened?

I see this:

ProblemReproducedConcurrencyYIeld.dfy(10,23): Error: invalid argument types (int and Box) to binary operator ==
1 type checking errors detected in problem__module.bpl

*** Encountered internal translation error - re-running Boogie to get better debug information

problem__module.bpl(3222,60): Error: invalid argument types (int and Box) to binary opera
tor ==
1 type checking errors detected in problem__module.bpl

I wanted the above to verify.

After investigation, it turns out that the override check is converting the ProblemHolder's postcondition to the Instantiation's functions and types, but the type of the function application is unchanged, resulting in a type parameter being boxed in one side of the equality and not the other one. Will fix soon.

What type of operating system are you experiencing the problem on?

Windows