Test that all primitive functions typecheck

[georgefst]

We attempt to check that, for every member of globalPrims, its declared type matches its behaviour.

This test is unfortunately extremely discard-happy, hence the withTests 1 currently. Generating complex expressions, then discarding those which are not normal form, is pretty inefficient. Ideally we'd have a generator which produces normal forms. It also always seems to stack overflow on Int.toNat for some reason - I haven't looked in to that.

If this is infeasible, it may be better to take a single arbitrary concrete value of that type. But this is far from ideal, since there there can be branches in the implementation of primFunDef e.g. for Int.rem.

Putting this here as a draft in case anyone has other ideas.

[georgefst]

Another alternative would be for EvalFull.binaryPrimTest, EvalFull.unaryPrimTest to also check the types. Our tests which use those are designed so that all branches in primFunDef should be exercised. We'd have to refactor them out ot the evaluation tests.

[brprice]

Ideally we'd have a generator which produces normal forms.

I'm guessing you need normal-in-an-empty-context, and only for a small set of types that can be (types of subterms of) arguments to primitive functions. I think this currently is only Char, Int and Nat. This seems pretty straightforward to do, as it is type-directed, and the only choices we ever have to make are "which of this small set of constructors should we use"?

[brprice]

This would (ideally) have caught the bug in #1159 . It does need to be a bit more nuanced than the above "generate a normal form", as const is now a primitive that does not require its arguments to be normal.

Having said that, the test is slightly redundant with the type preservation test, which did indeed catch the bug. However, a focused test would have caught it sooner, and could have given a much nicer failure report

[dhess]

Should we commit this in its current form anyway, then, despite the inefficiencies?

[brprice]

Should we commit this in its current form anyway, then, despite the inefficiencies?

I haven't looked at the code, but @georgefst says

It also always seems to stack overflow on Int.toNat for some reason - I haven't looked in to that.

So I think this at least needs to be addressed first