Variable lookup can fail for in Sequent.AST function constructTerm
In some cases when an argument cannot be inferred, the constructTerm
function has an in-exhaustive pattern.
We should investigate if there are cases which could be inferred better. If not then the user should be given indication of which operations have insufficient arguments so that these can be specified. (What part of the code should have this responisibility?)