error on function member combining datatype map with function

[erniecohen]

Dafny version

4.4.0

Code to produce this issue

type Kv = nat->nat
datatype T = T(
    m:map<nat,nat>
) {
    function apply(kv:Kv):Kv { k => if k in m then m[k] else kv(k) }
}

Command to run and resulting output

No response

What happened?

This gets the error "value does not satisfy the subset constraints of 'nat -> nat' (possible cause: it may be partial or have read effects)". (It should check without error.)

There is no error if m declared as a const or as a parameter. The error persists when kv is made a datatype field or an external const. The error disappears if kv(k) is replaced by 0, or if m[k] is replaced by 0.

(Incidentally, if error messages refer to read effects, they should be defined in the manual.)

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

Mac

[MikaelMayer]

Here is a workaround:

type Kv = nat->nat
datatype T = T(
    m:map<nat,nat>
) {
    function apply(kv:Kv):Kv { k => (if k in m then m[k] else kv(k)) as nat }
}

With the current type system, nat being a subtype, the if branch only assumes the base type. Weird encoding I know.

[keyboardDrummer]

You can also workaround this by adding an explicit type annotation for k: (k: nat)

@RustanLeino do you believe the type inference is not working as expected in this case? How come it does not infer k to be nat based on the applications of k to both m and kv ?

[RustanLeino]

This may be related to https://github.com/dafny-lang/dafny/issues/5244.

Perhaps the type inference can be improved to obtain a better type for the lambda expression. The new resolver always infers types of bound variables (like k in the example) as a base type (like int), never a subset type (like nat). This part is as intended. However, it would be nice if the body of the lambda could be inferred to be nat. I don't know why that's not happening, so I'd say that's a bug that's worthy of digging into.

[keyboardDrummer]

However, it would be nice if the body of the lambda could be inferred to be nat. I don't know why that's not happening, so I'd say that's a bug that's worthy of digging into.

It seems like the body is already inferred to be nat. The following programs works:

type Kv = nat->nat
datatype T = T(
    m:map<nat,nat>
) {
    function apply(kv:Kv):Kv { k => if k in m then m[k] else kv(3) }
}

The new resolver always infers types of bound variables (like k in the example) as a base type (like int), never a subset type (like nat).

Why is that? I surprises me so it feels like a bug.