Rebox rules violate ghc invariant

[mikesperber]

When running plugin output through -dcore-lint, we currently may get something like this:

*** Core Lint errors : in result of Simplifier ***
Bar.hs:25:1: warning:
    This argument does not satisfy the let/app invariant:
      case plus (I# 10#) (I# 1#) of { I# i#_aBa -> i#_aBa }
    In the RHS of foo :: Int
    Substitution: [TCvSubst
                     In scope: InScope {}
                     Type env: []
                     Co env: []]

This is because the reboxing rules are shaped like this:

rebox2" [~0] (+#) = \ u# v# -> unboxI (addC (boxI u#, boxI v#))

This rewrites, for instance, 10# +# 1# into case plus (I# 10#) (I# 1#) of { I# i#_aBa -> i#_aBa }). While the former is ok-for-speculation, the latter is not. (The lint error message might be different, but comes down to the same cause.)

See https://gitlab.haskell.org/ghc/ghc/-/issues/18677 for SPJ's take on this.

Now, the paper has an older version of these rules, which do not have this problem. This is preserved in Rebox.hs but #ifdefed out here:

https://github.com/conal/concat/blob/e71fe7dd73492abdfd432743ce2c1b249429fa5e/plugin/src/ConCat/Rebox.hs#L165

[conal]

Sadly, I do not remember why I changed the form of these rules. It might be just that I liked the more compact form (less boilerplate). Too bad I didn’t leave a comment behind.

I just ran stack build :gold-tests, then switched back to the earlier definitions and re-ran for comparison. I encountered some compilation errors:

• The “boxF log” rule was missing a parenthesis.
• GHC objected to the rules for log (on Float and Double), saying “RULE left-hand side too complicated to desugar”. Maybe this failure led me to the “Rebox” formulation that is now having troubles with speculation.

After restoring the missing parenthesis and commenting out the two log rules, I was able to compile. Re-running the gold tests, however, led to an error from the plugin “lam Case of boxer: bare unboxed var”, which means that my reboxing strategy failed. I think this failure was the main reason I switched strategies to the Rebox version, and avoiding the log failure was a fortunate byproduct.

My general intention in the plugin is to work with the flow of GHC. Every contradiction of GHC’s flow has led to complexity and brittleness. The whole “reboxing” issue is one of the few remaining failures to align with GHC. I’ve not yet figured out how to either (a) get GHC to delay unboxing until concat is done or (b) work with unboxed types in concat. The main obstacle to the latter route is that my category methods are polymorphic only over kind *, i.e., boxed types. I’d love to find a better solution!

[mikesperber]

So the above commit at least explains what immediately failed about going back to the rules from the paper:

The code from the plugin that replaces I#, D# etc. by boxI, boxD etc. was lost at some point. Putting it back in makes the rules fire, and at least the first few gold tests fire.

Alas, the magSqr test seems to loop with this.

[mikesperber]

I reverted the gold tests in

https://github.com/mikesperber/concat/commit/b3be49a4dac763622033d69a068d14fa1b07fc0d

to the HEAD version. They pass. I could swear magSqr looped before, but maybe I didn't wait long enough.

@conal Can you reproduce the failure you saw?

[conal]

@conal Can you reproduce the failure you saw?

I'm unclear on what failure you have in mind. In one version of the rules (old/paper, I guess) GHC refused to apply a few of the reboxing rules involving floating point and partiality.

[mikesperber]

@conal Above, you wrote "Re-running the gold tests, however, led to an error from the plugin “lam Case of boxer: bare unboxed var”. I can't reproduce this, at least not with the set of commented-in tests in HEAD. Do you remember what you did to produce this error?