Type compatibility PO does not get reported when invoking an operation

[peterwvj]

Consider the SL spec below

functions

funUseIdFun :  () -> nat
funUseIdFun () ==
let r : [nat] = nil
in
   idFun(r); --PO produced

idFun :  nat -> nat
idFun (x) == x;

The spec produces a single (reasonable) PO let r:[nat] = nil in is_(r, nat) saying that r must be a natural number when idFun is invoked.

Now consider an equivalent SL spec that uses operations to achieve the same:

operations

opUseIdOp :  () ==> nat
opUseIdOp () ==
let r : [nat] = nil
in
   return idOp(r);--No PO produced

idOp : nat ==> nat
idOp (x) == return x;

This spec does not produce any POs although you would expect a type compatibility PO similar to that shown above. I can also produce this issue using VDMJ (although it calls the PO a "subtype" PO rather than a "type compatibility" PO).

[nickbattle]

Looking at the VDMJ code (and I assume Overture is the same), the argument types are only checked if the apply expression is of a function, not an operation. I can't think why that would be, though it might be linked to the general principle, that I've mentioned before, that we can't do much with statements in the POG because we can't be sure of the context.

If you try this on VDMTools, you'll see the operation PO is just "is_nat(r)" - there is no "let" context to define r. I can make a simple change to VDMJ to do the same - and I think this would be reasonable. But there is still a wider issue about what we can and can't generate POs for within operation bodies.

[peterwvj]

Related to #466

Thanks for looking into this. I agree, I think it's reasonable to do what you are suggesting.

[nickbattle]

I have a patch for this, but it produces some unusual side effects. Need to look into it more closely before committing.