Type synonyms in `least`/`greatest` lemmas

[volodeyka]

Dafny version

4.11.0

Code to produce this issue

module Bug {

  newtype State = map<string, int>

  least lemma BugLemma(s: State)
  {
    assert s - {"x"} == s;
  }

}

Command to run and resulting output

What happened?

When I type in this code

module Bug {

  newtype State = map<string, int>

  least lemma BugLemma(s: State)
  {
    assert s - {"x"} == s;
  }

}

In Dafny, it complains that - application is illtyped:

type of right argument to - (set<seq<char>>) must agree with the result type (State)
type of - must be of a numeric type, bitvector type, ORDINAL, char, or a set-like or map-like type (instead got State)

However, if I change the newtype to just type, everything works

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

Mac