[Bug]: subset type for maps fails to verify overriden key/value pairs

[MikaelMayer]

Dafny version

3.9.1

Code to produce this issue

type foo = m: map<int, int> | forall n <- m.Keys :: m[n] < 5

function addToFoo(m: foo): foo
  ensures false
{
  m[1 := 7]
}

Command to run and results

dafny verify problem

Dafny produces 1 verified and 0 error.

What happened?

It should have verified that m[1 := 7] does not have necessarily the same type as m itself.

What type of Operating System are you seeing the problem on?

Linux, Windows, Mac, WSL

[cpitclaudel]

Two checks to add:

type seq0 = s: seq<int> | forall n <- s :: n == 0

function ReplaceInSeq0(s: seq0): seq0
  requires |s| > 0
  ensures false
{
  s[0 := 1]
}

type map0 = m: map<int, int> | forall k <- m :: m[k] == 0

function ReplaceInMap0(m: map0): map0
  requires 0 in m
  ensures false
{
  m[0 := 1]
}

The first one is already correctly rejected.

[robin-aws]

Fix should be similar to #2059

[MikaelMayer]

Two checks to add:

type seq0 = s: seq<int> | forall n <- s :: n == 0

function ReplaceInSeq0(s: seq0): seq0
  requires |s| > 0
  ensures false
{
  s[0 := 1]
}

type map0 = m: map<int, int> | forall k <- m :: m[k] == 0

function ReplaceInMap0(m: map0): map0
  requires 0 in m
  ensures false
{
  m[0 := 1]
}

The first one is already correctly rejected.

I added these two examples to the PR