pact icon indicating copy to clipboard operation
pact copied to clipboard

typecheck does not work with wrong arg count

Open Divesh-Otwani opened this issue 2 years ago • 3 comments

Issue description

If I call a function in an external module with the wrong number of arguments, this won't be detected by the typechecker.

Steps to reproduce

bad-typecheck.pact

(namespace "free")
(module bad-typecheck GOV
  (defcap GOV () true)
  (defun should-fail (x:integer)
    (free.helper.helper x)
  )
)

helper.pact

(namespace "free")
(module helper GOV
  (defcap GOV () true)
  (defun helper:string (x:integer y:string) (format "{} of {}" [x y]))
)

bad-typecheck.repl

(begin-tx)
(env-data {"ns-ks":["ns-key"]})
(env-sigs [{"key":"ns-key", "caps":[]}])
(define-namespace "free" (read-keyset "ns-ks") (read-keyset "ns-ks"))
(load "helper.pact")
(load "bad-typecheck.pact")
(typecheck "free.bad-typecheck")
(print (expect-failure "wrong num of args" (free.bad-typecheck.should-fail 3)))
(commit-tx)
divesh:issue$ pact bad-typecheck.repl
Expect failure: success: wrong num of args
Load successful

Expected Behavior

The line (typecheck "free.bad-typecheck") should display the error that we call helper with the wrong number of arguments.

Divesh-Otwani avatar May 31 '23 19:05 Divesh-Otwani

Reduced example (note, that I have annotated should-fails type):

(module m G (defcap G () true)
        (defun helper:string (x:integer y:string) (format "{} of {}" [x y]))
        (defun should-fail: string (x:integer)
               (helper x)))

(typecheck 'm)

Output:

"Loaded module m, hash 9rbppHYjW2Q9uDnjtsfdfxIvTxyy9qxtYOVbRX-MGMk"
"Typecheck m: success"

rsoeldner avatar May 31 '23 20:05 rsoeldner

Reduced example (note, that I have annotated should-fails type):

(module m G (defcap G () true)
        (defun helper:string (x:integer y:string) (format "{} of {}" [x y]))
        (defun should-fail: string (x:integer)
               (helper x)))

(typecheck 'm)

Output:

"Loaded module m, hash 9rbppHYjW2Q9uDnjtsfdfxIvTxyy9qxtYOVbRX-MGMk"
"Typecheck m: success"

Ah ... so it doesn't depend on using another module. I thought it did because that's the only place I noticed it in my pact work. Here's the repl version:

(begin-tx)
(module m G (defcap G () true)
        (defun helper:string (x:integer y:string) (format "{} of {}" [x y]))
        (defun should-fail: string (x:integer)
               (helper x)))
(typecheck "m")
(print (expect-failure "wrong arg count" (m.should-fail 3)))
(commit-tx)

Divesh-Otwani avatar May 31 '23 20:05 Divesh-Otwani

This seems to point to a discrepancy in the runtime tc vs the static tc. The expression (helper x) doesn't seem to track saturation in the static tc, just the type of the thing it's "supposed" to return via the type of the body, as evidenced by:

pact> (m.helper 3)
<interactive>:0:0:Error: helper: Incorrect number of arguments (1) supplied; expected 2

@jmcardon is going to get started reworking the typechecker, but I'll see if i can't track down the problem when I get back.

emilypi avatar Jun 01 '23 19:06 emilypi