saw: user error (Could not create sbv argument for Cryptol.TCSeq [_,_])

[weaversa]

I don't have an example. Also, contrary to the message, I don't think the error is my fault...

[brianhuffman]

This sounds a lot like issue #60, which arises when you have uninterpreted functions with polymorphic types. Is this a duplicate, or something else?

[weaversa]

I was uninterpreting a polymorphic cryptol function...but the function was monomorphic in the context it was called in. It was something like:

f : {a} -> Type a -> [32] -> [32]
f t x = t.a + x

g x = f concreteType x

...
returns {{ g x }};
unint_z3 ["f"];
...

If this isn't enough, I can try to make a real example...It seemed to me that I was uninterpreting a polymorphic function, but in the context, every call to it was monomorphic.

[brianhuffman]

Duplicate of #60.