Fix empty list translation

[rsoeldner]

Fixes #1182

Prior this PR, the following code

(module test G
  (defcap G () true)

  (defun test:[string] (x: [string])
         @model [(property (= x x))]
         (let ((default-val:[string] [])) default-val)
         x)
  )

(verify 'test)

ended in a execution error (Z3 error):

"Loading fv.repl..."
"Loaded module test, hash 0zf1WbH8tKfNC1OU58opdF_uOC-JSuBPg7-tmrGM9PA"
"Verification of test failed"
fv.repl:5:27:OutputFailure: 
*** Data.SBV: Unexpected non-success response from Z3:
***
***    Sent      : (define-fun s7 () Bool (= s1 s6))
***    Expected  : success
***    Received  : (error "line 23 column 32: Sorts (Seq String) and (Seq Any) are incompatible")
***
***    Exit code : ExitFailure (-15)
***    Executable: /usr/bin/z3
***    Options   : -nw -in -smt2
***
***    Reason    : Check solver response for further information. If your code is correct,
***                please report this as an issue either with SBV or the solver itself!

The reason for this behavior is the way we handle the empty list inside mkLiteralList, which returns a list literal of type Any for the empty list.

With the proposed changes, the verification passes as expected:

 (load "fv.repl" )
"Loading fv.repl..."
"Loaded module test, hash 0zf1WbH8tKfNC1OU58opdF_uOC-JSuBPg7-tmrGM9PA"
"Verification of test succeeded"

PR checklist:

• Test coverage for the proposed changes
• PR description contains example output from repl interaction or a snippet from unit test output
• Documentation has been updated if new natives or FV properties have been added. To generate new documentation, issue cabal run tests. If they pass locally, docs are generated.
• Any changes that could be relevant to users have been recorded in the changelog
• In case of changes to the Pact trace output (pact -t), make sure pact-lsp is in sync.

Additionally, please justify why you should or should not do the following:

• Confirm replay/back compat
• Benchmark regressions
• (For Kadena engineers) Run integration-tests against a Chainweb built with this version of Pact

[jwiegley]

Why is it called retTy here? What is node at this point?

[rsoeldner]

retTy is the return type of the translation step, i.e. SList SStr. I will change it to listTy.

The node is of type Node from the Typecheck module, see here. For the particular example above, its TyList {_tyListType = TyPrim TyString}.

Need answer to a question first, I realized

[rsoeldner]

The macOS test is probably failing due to an historical version of Z3. In #1226 we bump the version.

[imalsogreg]

May be nice for the description to be self-contained.

[emilypi]

LGTM thank you for the regression.