The set passed to <:, <-:, :-> and :> operators can be of an arbitrary type. The operator does not have to succeed in limiting the map - it may be that no entries in the set match the map or the set may be empty. Currently the 3.0.3 type checker is over-constraining these set values to match the type of the map that they are operating on. This was fixed in VDMJ at some point, but Overture missed it.
The set passed to
<:
,<-:
,:->
and:>
operators can be of an arbitrary type. The operator does not have to succeed in limiting the map - it may be that no entries in the set match the map or the set may be empty. Currently the 3.0.3 type checker is over-constraining these set values to match the type of the map that they are operating on. This was fixed in VDMJ at some point, but Overture missed it.