Strict typechecking mode

[jneem]

This adds a --strict-typechecking flag that starts the typechecker in "checking" mode, equivalent to wrapping each file in (...) : _.

A couple of points I was unsure of:

• this PR does it for every file, but maybe we only want it at the top level?
• I noticed while testing that despite the "strict" in the name, it's sometimes more permissive than non-strict mode (because of type inference; see the added tests). Maybe "strict" mode should run both kinds of typechecking so it's actually strictly stricter?

Fixes #2049

[github-actions]

Bencher Report

Branch	2077/merge
Testbed	ubuntu-latest

⚠️ WARNING: The following Measure does not have a Threshold. Without a Threshold, no Alerts will ever be generated!

• Latency

Click here to create a new Threshold
For more information, see the Threshold documentation.
To only post results if a Threshold exists, set the --ci-only-thresholds CLI flag.

Click to view all benchmark results

Benchmark	Latency	nanoseconds (ns)
fibonacci 10	📈 view plot ⚠️ NO THRESHOLD	494,100.00
foldl arrays 50	📈 view plot ⚠️ NO THRESHOLD	1,771,100.00
foldl arrays 500	📈 view plot ⚠️ NO THRESHOLD	6,748,500.00
foldr strings 50	📈 view plot ⚠️ NO THRESHOLD	7,256,500.00
foldr strings 500	📈 view plot ⚠️ NO THRESHOLD	63,521,000.00
generate normal 250	📈 view plot ⚠️ NO THRESHOLD	46,735,000.00
generate normal 50	📈 view plot ⚠️ NO THRESHOLD	2,101,700.00
generate normal unchecked 1000	📈 view plot ⚠️ NO THRESHOLD	3,247,200.00
generate normal unchecked 200	📈 view plot ⚠️ NO THRESHOLD	749,480.00
pidigits 100	📈 view plot ⚠️ NO THRESHOLD	3,230,800.00
pipe normal 20	📈 view plot ⚠️ NO THRESHOLD	1,490,300.00
pipe normal 200	📈 view plot ⚠️ NO THRESHOLD	10,218,000.00
product 30	📈 view plot ⚠️ NO THRESHOLD	831,740.00
scalar 10	📈 view plot ⚠️ NO THRESHOLD	1,516,400.00
sum 30	📈 view plot ⚠️ NO THRESHOLD	830,670.00

🐰 View full continuous benchmarking report in Bencher

[yannham]

I noticed while testing that despite the "strict" in the name, it's sometimes more permissive than non-strict mode (because of type inference; see the added tests). Maybe "strict" mode should run both kinds of typechecking so it's actually strictly stricter?

I think it's fine as it is; it's the expected semantics (as you say, it behaves is if we put : _ every where at the top of each file), and while it's more permissive, it's not accepting dubious programs. I would say that it's smarter rather than just more permissive.

Regarding tests, maybe we should add a test that imports are also properly strictly typechecked.

[yannham]

Nitpick: there is an enum typecheck::pattern::TypecheckMode = { Walk, Enforce }. Maybe it would be better to use that instead of a boolean (boolean blindness and all that) ? In that case maybe hoist it up in the typecheck module, because it's not for patterns only anymore.

[yannham]

I think it's fine as it is; it's the expected semantics (as you say, it behaves is if we put : _ every where at the top of each file), and while it's more permissive, it's not accepting dubious programs. I would say that it's smarter rather than just more permissive.

Ok but now maybe I see your point: it might be surprising that some files require --strict-typechecking to work. On the other hand it would be sad and wasteful to just run typechecking a second time in walk mode. I'm tempted to say that it's on the user. Maybe providing a way to do the same thing with a pragma located in the file instead would be more resilient to this kind of issues, as now the decision is taken by the source program and not the invoker of the CLI?

[jneem]

I was mainly thinking from the point of view of someone wanting to run extra checks in CI. There, you don't really care if nickel typecheck is a little (or even a factor of 2) slower, but you'd be surprised if it misses out on some problems that are caught by a "normal" typecheck. I'm not sure that having pragmas in the file really solves this use case, though: I'm imagining that I have a normal nickel file that isn't supposed to need any special settings, and I just want to run some extra-strict checks on it.

[yannham]

Hmm, indeed.

By the way, should we make --strict-typechecking an argument of nickel typecheck only? Maybe that would make it clear that this is some kind of separate check, and then it would be acceptable to run typechecking in both mode - we don't penalize normal execution, which is what matters probably. In that case I tend to agree that maybe the double run is what you want.

And if it starts to be too slow, we can easily make it so that the typechecker just ignores any expression with a type or a contract annotation on the second run (some kind of shallow walk,so to speak), to make sure it doesn't duplicate any work from the strict pass.

Another solution would be to rerun the typechecker in strict mode upon failure in normal execution: if the program is typeable with a bit more effort, then we accept it. But I'm not sure it's such a good idea: if people start to rely on this behavior, then the default path would waste work in the first attempt at each execution.

[yannham]

And if it starts to be too slow, we can easily make it so that the typechecker just ignores any expression with a type or a contract annotation on the second run (some kind of shallow walk,so to speak), to make sure it doesn't duplicate any work from the strict pass.

Wait, we can't do that, because that won't catch your example. Maybe the converse is fine though: first run the normal pass, and for the strict pass, only reprocess what was untyped before? Since inference is more powerful, it seems like if a typed block passes the normal phase, then it would necessarily pass the strict one. Would have to think a bit harder to make sure.