SAWCore term mysteriously goes out of scope if given a certain type

[RyanGlScott]

For some reason, SAW accepts this program:

let identity = parse_core "\\(x : Integer) -> x";
prove_print z3 {{ \x -> identity x == x }};

But it does not accept it if identity is given a slightly different type:

let identity = parse_core "\\(x : Nat) -> x";
prove_print z3 {{ \x -> identity x == x }};

[15:43:59.027] Loading file "/home/rscott/Documents/Hacking/SAW/Bug.saw"
[15:43:59.035] Cryptol error:
[error] at /home/rscott/Documents/Hacking/SAW/Bug.saw:2:25--2:33
    Value not in scope: identity

I'm not sure if this is intended to work or not, but if not, the error message doesn't indicate why.

[RyanGlScott]

In case it's important, I'm using SAW at commit e8703733 in https://github.com/GaloisInc/saw-script/issues/1348#issue-926355798. If I use the saw-0.8 release, it panics:

[15:45:11.894] Loading file "/home/rscott/Documents/Hacking/SAW/Bug.saw"
[15:45:11.894] You have encountered a bug in cryptol-saw-core's implementation.
*** Please create an issue at https://github.com/GaloisInc/saw-core/issues

%< --------------------------------------------------- 
  Revision:  e4c59543fc7520d6cfa3d44b0602a3274685b35d
  Branch:    HEAD
  Location:  scCryptolType
  Message:   scCryptolType: unsupported type (x : Prelude.Nat)
-> Prelude.Nat
CallStack (from HasCallStack):
  panic, called at src/Verifier/SAW/Cryptol/Panic.hs:13:9 in cryptol-saw-core-0.1-inplace:Verifier.SAW.Cryptol.Panic
  panic, called at src/Verifier/SAW/Cryptol.hs:1608:13 in cryptol-saw-core-0.1-inplace:Verifier.SAW.Cryptol
%< ---------------------------------------------------

[robdockins]

This was changed recently by #1336. Basically, the issue is that Nat -> Nat doesn't correspond to any Cryptol type. This used to panic, as you can see. Now, SAWCore terms that don't have types that can be understood as Cryptol types are simply not put into the Cryptol environment.

I don't know offhand of a great way to improve the situation WRT the error message.

[RyanGlScott]

Hm, OK. But identity is in a SAW environment of some sort, right? After all, I can do things like:

sawscript> print_term identity;
[16:50:30.629] \(x : Nat) -> x

Would it suffice to check for identifiers that are present in this environment but not present in the Cryptol environment, and if so, give a more specific error message?

[robdockins]

The name resolution at that point is done by the Cryptol renamer; it doesn't know anything about the SAW environment, so it would be hard to do it at the time of lookup. I don't know offhand how a "not in scope" error is propagated, but we could potentially catch it and check if the identifier is in the SAW environment and print a different message.

[atomb]

This would be helped by having Cryptol always return structured error types, rather than textual messages, all the way up to the top level, so the SAWScript REPL could inspect what type of error occurred.