type-directed compilation

[flupe]

A big refactoring as a first step to properly handle module parameters.

The most important change is the following: the compilation of terms if now completely type-directed. That is, we no longer rely on ArgInfo of Elims to know whether they have to be preserved, but rather their Dom Type only.

What this means, concretely:

• Explicit usable erasable arguments (Say, (a : Set)) are dropped.
• Implicit usable non-erasable arguments (Say, {x : Nat}) are made explicit.
  (This means we now officially support tactic arguments that are made explicit on the Haskell side.)

As a treat, we now properly erase types of sort Prop.

Closes #217.

---

TODO list before opening the PR:

• Add back special class functions.
• Fix compilation of co-patterns.
• Fix compilation of patterns on projection-like functions.
• Add back compilation of inline functions.
• Ensure unfolding is back.
• Drop module parameters again.

[flupe]

All the tests pass again, finally.

Before merging this PR, there's still one caveat to fix: currently every test has the flag --no-projection-like set, because projection-like are annoying to manipulate.

The following things are likely to break once I remove the flag:

• Compilation of functions, as projection-like only store patterns that come after the record argument.
• Compilation of Defs, because some defs will be compiled in compileProj.
• compileSpined?

[jespercockx]

Great work! This is definitely a major improvement to the compilation process of agda2hs. Going through the changes also made me realize that we're really not dealing with a small project here anymore. I have a couple of remarks and I think the projection-like functions should still be fixed. But overall I think this should be merged sooner rather than later.

[flupe]

Thanks for the review! My git skills are fairly limited but you're right that making another PR for purely cosmetic refactorings would be better. I'll see what I can do.

[flupe]

Rebased on #277.

[omelkonian]

Great work Lucas!

One thing that slightly worries me is that I would expect this refactoring to reduce code size, but it in fact increases it substantially (c.f. +800/-500). Factoring out new tests and utilities we did not need before, it seems the main culprit is Compile.Term; do you think the final polished version might be able to reduce LOC down a bit?

PS: Ping me when the projection-like optimization has been properly handled.

[naucke]

Implicit arguments with instance functions are still a compiler error, is this expected? i.e.

test : {x : Nat} → Nat
test {x} = x
{-# COMPILE AGDA2HS test #-}

will work but

instance
  test : {x : Nat} → Nat
  test {x} = x
{-# COMPILE AGDA2HS test #-}

will give

An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/Agda2Hs/Compile/ClassInstance.hs:103:20 in main:Agda2Hs.Compile.ClassInstance

[flupe]

Hmm, to be fair the compilation of class instances is the part I'm the least happy with currently (the current implementation and what I did to make it typed).

Though I fail to see when a compiled instance with hidden relevant arguments turning relevant would ever make sense. I will add a check that for instances specifically, no relevant arguments are ever hidden as I think this would do the trick. Thanks for the example!

If you ever encounter an example where this would be useful behavior, hit me up!

[naucke]

I came across this experimenting with adding runtime checks for e.g. erased preconditions. A deciding version of a precondition would ideally be written as instance so it can be found in instance search:

instance
  decLt : {x y : Nat} → Haskell.Extra.Dec.Dec (x Data.Nat.< y)
  decLt {x} {y} = (x Haskell.Prelude.< y) ⟨ … ⟩

subtractFromGreater : (x y : Nat) → (@0 checkThis : x Data.Nat.< y) → Nat
subtractFromGreater x y lt = _-_ y x ⦃ … ⦄

{-# COMPILE AGDA2HS subtractFromGreater rtc checkThis #-}

then decLt can be found through instance search for the precondition checkThis, which is a little nicer.

[flupe]

@omelkonian: I fixed the compilation of projection-like functions and addressed all of your comments!

You will see that one test still requires the --no-projection-like flag as compiling projection-like (or projections) directly applied to constructors in a typed setting kinda goes against bidirectional tc. Quoting @jespercockx:

a projection-like function applied to a constructor violates bidirectionality so you cannot (easily) do a type-aware traversal of it

If you remove the flag, the code will still compile to correct Haskell, but the projection-like function unbind will get reduced. Not incorrect, but just not what the user wrote.

If someone is really motivated, perhaps using projView could allow you to preserve the projection-like function application, but I think you'd still have to trigger inference at some point, which I don't want to do.

One thing that slightly worries me is that I would expect this refactoring to reduce code size, but it in fact increases it substantially (c.f. +800/-500). Factoring out new tests and utilities we did not need before, it seems the main culprit is Compile.Term; do you think the final polished version might be able to reduce LOC down a bit?

Hm, going into this implementation I had the same assumption, but quickly realized some more work was unavoidable (e.g Defs and projections cannot really be treated uniformly anymore).
All in all, I don't think too much code is added, there is also a lot of whitespace introduced because I like my code to breathe.

Hopefully things should be more easily maintainable too :)

---

@jakobn-ai: came across this experimenting with adding runtime checks for e.g. erased preconditions. A deciding version of a precondition would ideally be written as instance so it can be found in instance search: [...]

But the instance itself shouldn't be compiled to agda2hs right? Or using some custom logic (that you'd have to implement yourself).

I decided against adding the check I mentioned above, since the class compilation routine already doesn't enforce that, say, we don't pattern-match on parameters of instances, and they are silently dropped til we reach a (class) projection (See here).

So something should be done alright, just not in this PR!

[omelkonian]

If you remove the flag, the code will still compile to correct Haskell, but the projection-like function unbind will get reduced. Not incorrect, but just not what the user wrote.

Could you also add these unit tests, i.e. the ones without the flag where the generated code is further away from what the user wrote?

Then, a subsequent PR that improves on that (e.g. using projView) could improve those tests.

[flupe]

Done! (See test/ProjLike.agda)