Cryptol-saw-core translator produces ill-typed terms from polymorphic recursive functions

[brianhuffman]

This problem was discovered as a test suite failure in #1317, which bumps cryptol to include the new sortBy function in the Cryptol prelude. Here's a self-contained example that you can do from the REPL:

sawscript> let {{ funpow f (n : Integer) x = if n <= 0 then x else funpow f (n - 1) (f x) }}
sawscript> type {{ funpow }}
[18:30:50.891] {a} (a -> a) -> Integer -> a -> a
sawscript> check_term {{ funpow }}

Stack trace:
"check_term" (<stdin>:1:1-1:11):
Inferred type
  sort 1
Not a subtype of expected type
  sort 0
For term
  (u957 : sort 0)
-> (u957
    -> u957)
-> Prelude.Integer
-> u957
-> u957

[robdockins]

It looks well-typed to me. I think the problem is just expecting it to have sort 0.

[brianhuffman]

I believe that the primitive fix (which is used to translate recursive functions) just has a too-restrictive type:

saw-script/saw-core/prelude/Prelude.sawcore

Line 19 in 03b0fa8

primitive fix : (a : sort 0) -> (a -> a) -> a;

I think the type error message is really complaining about the argument to fix having the wrong type (sort 1 vs the expected sort 0 for argument a). By the way, we should try to include more location information on such error messages so that I don't have to guess about things like that.

[brianhuffman]

Indeed, changing the type of fix to (a : sort 1) -> (a -> a) -> a fixes the problem:

sawscript> let {{ funpow f (n : Integer) x = if n <= 0 then x else funpow f (n - 1) (f x) }}
sawscript> check_term {{ funpow }}
[18:40:25.702] (u957 : sort 0)
-> (u957
    -> u957)
-> Prelude.Integer
-> u957
-> u957

The more general type is absolutely necessary if we want to be able to handle polymorphic recursion.