FV type inference of function result not properly working

[rsoeldner]

Within the formal verification module, the type inference of the function result body, and hence the result property, is not properly working.

The following type error:

"Verification of test failed"
:OutputFailure: pact-issue-1107.repl:5:23: could not parse (> result 0.0): in (> result 0.0), type error: * vs decimal (CallStack (from HasCallStack):   typeError, called at src-tool/Pact/Analyze/Parse/Prop.hs:452:16

Can be generated by running:

(module test GOVERNANCE
  (defcap GOVERNANCE() true)

  (defun get-refund (balance:decimal stakers:integer)
    @model [ (property (> result 0.0)) ]

    (enforce (> balance 0.0) "balance must be non-negative")
    (enforce (> stakers 0) "stakers must be non-negative")
    
    (/ balance stakers)))

(verify 'test)

The issue can be fixed by explicitly annotating the function return type (decimal).

I tried tracking town the issue, and it seems to me that in getFunChecks, we

1. collect function types (funTypes)
2. collect the set of checks for each function (moduleFunCheck)

Already here, the function type map lists the return type as TyVar:

FunType {_ftArgs = [Arg {_aName = "balance", _aType = TyPrim TyDecimal, _aInfo = balance},Arg {_aName = "stakers", _aType = TyPrim TyInteger,                                                                                                                                                                 
_aInfo = stakers}], _ftReturn = TyVar {_tyVar = TypeVar {_tvName = "b", _tvConstraint = []}}}

In moduleFunCheck here, we use makeFunctionEnv which binds the result type to SAny (here).