Make check_ir dump upon failure and call Check_ir only from pipeline

[nomeata]

Call Check_ir only from pipeline

this greatly simplifies many module interface

• no need to pass Typing.scope to transformations
• no need for them to import Check_ir
• Check_ir is now just a single function.

This does away with the higher-order hook check_exp in Check_ir.exp
and replaces it with Ir.flavor, a record describing the particular
“flavor” at this point. This has also the advantage that Check_ir
would notice if a pass after, say, Async would re-introduce calls to
async.

Make check_ir dump upon failure

and other improvements cherry-picked from #171 and #146, namely:

• add an interface file (and remove code known to be dead)
• make the Check_ir.env abstract

[nomeata]

Also nicer printing of subtype failure; multi-line really helps here.

[crusso]

This is generally ok, though I prefer the flexibility of passing in flavor checker so you can completely decouple the general type checker from other passes (eg. experimental ones like show).
Indeed, we could imagine composing the checker functions to maintain invariants established by previous passes. Perhaps one could just add a custom flavour to the variant that allows one to do this.

However, there is one issue, noted in issue https://dfinity.atlassian.net/browse/AST-35.
We currently split the transformation of the prelude and program and that can break whole program transformations (such as Async.ml) if we extend the prelude with constructs that require transformation (async T). Perhaps the correct thing to do is to apply all the transformations to the prelude and program separately and hope that they are compositional. Even better, apply the transformation in one step to the entire program and make the compiler discover and duplicate the prelude (and libraries) as necessary.

[crusso]

Silly idea perhaps but we could put a partial order on flavors, record the flavor in the output of the pass and check the invariants of all flavours before the current flavour. So desugar < async < await < tailcall compilable. Probably not worth it though...

[crusso]

Oops, I didn't review careful enough - you are actually doing the partial ordering already using a Boolean lattice (I guess). Nice!

[crusso]

maybe has_async_typ is more descriptive
also what is has_loop? Is that for tailcalls or anticipating Matthew's loop simplication?

[nomeata]

maybe has_async_typ is more descriptive

Yup.

Is that for tailcalls or anticipating Matthew's loop simplication?

The latter. I was too lazy to put in the actual checks yet, and will leave that to be done in #146.

[nomeata]

Indeed, we could imagine composing the checker functions to maintain invariants established by previous passes.

I considered this, but found it overkill to just disable certain constructors.

Perhaps the correct thing to do is to apply all the transformations to the prelude and program separately and hope that they are compositional.

We should do that. We need that anyways once we have separate compilation of modules.