Deriving `false` with sequence subtypes

[volodeyka]

Dafny version

4.11.0

Code to produce this issue

module Foo {
  newtype pos = i: seq<nat> | |i| > 0 witness [0]
}

module Bar {
  import Foo

  function Bar(n: nat): Foo.pos {
    seq(n, i => i)
  }

  lemma False()
    ensures false
  {
    assert |Bar(0)| > 0;
  }
}

Command to run and resulting output

What happened?

In the code snippet above, I can derive false. It seems to me like Dafny might be forgetting to check subtype constraints for seq comprehensions.

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

Mac