Type checking sometimes doesn't terminate when using `--type-system-refresh`

[dschoepe]

Dafny version

4.6.0+7c82175da631d3fdc3acea92a3614d66a3fdf7f2

Code to produce this issue

trait SomeTrait<T> {
  function f(): (res: T)
}

// doesn't terminate:
// class Bar {}
type Bar = nat
// terminates:
// type {:extern} Bar
// datatype Bar = Bar

// hangs:
datatype Option<+U> = None | Some(val: U)
// terminates:
// datatype Option<U> = None | Some(val: U)

method foo(v: Option<SomeTrait<Bar>>)
{
  var _ := match v {
    case Some(s) => Some(s.f())
    case _ => None
  };
}

Command to run and resulting output

dafny resolve --type-system-refresh DafnyTerminationBug.dfy

What happened?

The above command does not seem to terminate. Changing to any of the commented out options for Bar or changing the variance for Options type parameter from +U to U makes the program resolve successfully.

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

Linux, Mac

[stefan-aws]

I can confirm the behaviour on my Mac in VSCode with Dafny 4.6.0.