kadena-io / pact

The Pact Smart Contract Language
https://docs.kadena.io/build/pact
BSD 3-Clause "New" or "Revised" License
584 stars 102 forks source link

typecheck does not work with wrong arg count #1236

Open Divesh-Otwani opened 1 year ago

Divesh-Otwani commented 1 year ago

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.

rsoeldner commented 1 year ago

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"
Divesh-Otwani commented 1 year ago

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)
emilypi commented 1 year ago

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.