Cryptol error: Incorrect type form. Expected: a value type Inferred: a numeric type)

[weaversa]

What is going wrong here?

sawscript> let f (x : Int) = eval_int {{ `x : [32] + 1 }}
sawscript> :t f
Int -> Int
sawscript> :t 10
Int
sawscript> :t f 10
Int
sawscript> f 10

user error ("f" (<stdin>:1:1-1:2):
Cryptol error:
[error] at <stdin>:1:36--1:44:
  Incorrect type form.
    Expected: a value type
    Inferred: a numeric type)

[weaversa]

I found the problem, a lack of parens...though I don't think the parens should be necessary.

sawscript> let a x = if (eval_bool {{ `x : [32] == 0 }}) then 1 else 0
sawscript> a 1

user error ("a" (<stdin>:1:1-1:2):
Cryptol error:
[error] at <stdin>:1:33--1:42:
  Incorrect type form.
    Expected: a value type
    Inferred: a constraint)
sawscript> let a x = if (eval_bool {{ (`x : [32]) == 0 }}) then 1 else 0
sawscript> a 1
[20:39:44.152] 0

[weaversa]

This seems to be a cryptol thing, rather than saw.

[weaversa]

Well, it is kind of strange that saw blindly accepts anything in double curly braces...

sawscript> let f a = {{ 1a1lsdkjl ())))(()asdkjf lasjd f' }}
sawscript> :t f
{a.0} a.0 -> Term

[brianhuffman]

That's because saw doesn't actually parse the contents of those {{ }} strings until they are actually used. We could catch some errors earlier by running them through the cryptol parser during saw-script type checking (i.e. when a saw-script function is declared). But we have to delay cryptol type checking until the saw-script function is called, because the type-correctness of those cryptol expressions can depend on the particular values of the numeric parameters.

If you'd like to get the cryptol parse errors earlier, just open a separate ticket and we can make that change.

[brianhuffman]

Another comment about the need for parens in expressions like (x : [32]) + 1: Currently in the cryptol grammar the : has lower precedence than other infix operators for types or expressions. I think this is a reasonable choice. The alternative would be to require parentheses in things like f : ([8] -> [8]) (similarly if you replace -> with whatever user-defined infix type operator you like). Or I suppose you could give a precedence for : that is lower than some operators but higher than others, but that would really mess up the grammar (we would not be able to distinguish between expressions and types until fixity resolution time) and I think it would also be confusing (basically for the same reason).