Run CI with typechecking after each desugaring pass?

[jamescheney]

Right now can enable typechecking after each desugaring pass, however, if this is enabled in the test run done by CI, it times out because re-typechecking takes too long.

We could do this if sufficient efficiency improvements were made to typechecking, or perhaps by caching/separate compilation so that prelude.links doesn't get re-typechecked over and over.

[jamescheney]

As of 2b26e2fe59a647cb08382bbe26f3fa35c37887f1 we are now doing this for just the prelude.links (not for all examples). So, I propose we close this, since there currently doesn't seem to be a prospect of making revalidation fast enough for it to be viable to do for all of the tests.

Instead, I suggest we do full revalidation tests off-line and whenever we encounter a problem, add a new test to recheck_frontend_transformations.tests to fully revalidate in the same way as prelude.links is handled now.

[jstolarek]

Maybe we could also enable recheck_frontend_transformations in the examples_default.config. That requires that we fix #871 first (because now the prelude does not typecheck) and investigate performance impact.

[dhil]

Toggling recheck_frontend_transformations=true produces the following errors on my machine when running test-harness tests/typecheck_examples.tests.

examples/crop.links:85: Type error: Because of the value restriction there can be no
examples/relational_lenses/cds.links:21: Type error: The functional dependencies do not specify that the drop columns are defined by the key columns.
examples/sessions/bookshop-cp.links:80: Type error: The cases of an offer should match the type of its patterns, but the pattern
examples/sessions/Elvina/Bookshop_CP.links:84: Type error: The cases of an offer should match the type of its patterns, but the pattern
examples/sessions/fuse-cp.links:16: Type error: Only dual session types can be linked, but the type
...
!FAILURE: Typecheck example file examples/mvu/mousetest.links [TIMED OUT]
!FAILURE: Typecheck example file examples/mvu/time.links [TIMED OUT]
!FAILURE: Typecheck example file examples/mvu/pong.links [TIMED OUT]
!FAILURE: Typecheck example file examples/mvu/todomvc/todoMVC.links [TIMED OUT]
!FAILURE: Typecheck example file examples/mvu/keypress.links [TIMED OUT]
!FAILURE: Typecheck example file examples/mvu/commands.links [TIMED OUT]

[jamescheney]

Toggling recheck_frontend_transformations=true produces the following errors on my machine when running test-harness tests/typecheck_examples.tests.

I just tried this and it seems there are even more errors now.

This is quite an old issue and it seens that it would require a concerted effort to fix the various issyes that make typechecking/inference not succeed after the various desugaring steps.

I think art of the reason for this is that type inference is not "idempotent" in the sense that rerunning even without doing any transformation isn't guaranteed to work. This leads to error messages like:

examples/crop.links:85: Type error: Because of the value restriction there can be no
free rigid type variables at an ungeneralisable binding site,
but the type `Process ({ |hear:[|MouseDown:(Int, Int)|MouseMove:(Int, Int)|MouseUp:(Int, Int)|StartResize:[|NE|NW|SE|SW|]|a|]|b})' has free rigid type variables.
In expression: var frameMgr = spawnClient {frameMgr(left, top, left, top, width, height)};.')

One solution would be to "clean" the AST after each desugaring step and rerun type inference from scratch, that is not what we are currently doing though.

I think the right way to go about this would be to annotate the source ASTs with type information after type inference ust once, and then transform/maintain this through the desugaring stages until translation to typed IR. This could either be by modifying type inference to make it idempotent by reusing type annotations that are already there correctly, or writing a checker for annotated post type inference ASTs.

So I suggest we close this, and perhaps create separate bug issues about each of the specific problems we see when rechecking after desugaring.

[dhil]

I think the right way to go about this would be to annotate the source ASTs with type information after type inference [...] This could either be by modifying type inference to make it idempotent by reusing type annotations that are already there correctly [...]

I agree with the basic idea. I would like to see some kind of monotonicity property, i.e. adding correct type annotations to a type-inferrable program always renders the annotated program type-inferrable.

[jamescheney]

Another thing to keep in mind is that as per #969, we currently have some desugaring passes that introduce flexible type variables (because they don't know what else to do) and thus generate code that doesn't translate to typable IR without further work, e.g. by rerunning type inference.

I don't have the details of what is going on with #969 paged in, but one sensible thing to do might be to adjust type inference to be idempotent, using whatever annotations are already present and inferring/instantiating where this is not the case. However, there may be a better way around #969. I'm mostly writing this to record that there are some parallel issues here, to be taken into account when/if we redesign or rationalize type inference/checking and its interaction with desugaring passes.