Tests fail on GHC 7.10.2

[RyanGlScott]

Well, that can't be good.

Related: the tcl_loc field of TcLcEnv had its type changed from SrcSpan in 7.10.1 to RealSrcSpan in 7.10.2, so I had to make a small tweak to HERMIT. I tried to model the change based on how GHC handles things for GHCi, but I can't vouch for its correctness.

[andygill]

It looks like one of the RULES is disappearing in the first failing test. I'm going back to HERMIT (non-shell) to track this down.

[andygill]

When tracking down the rules:

hermit<21> show-rule "repH ++"
∀ △ xs ys.
repH ▲ (augment ▲ (λ △ c n → foldr ▲ ▲ c n xs) ys)
≡
let f = repH ▲ xs
    g = repH ▲ ys
in λ x → f (g x)

but the RULE is:

{-# RULES "repH ++" forall xs ys .     repH (xs ++ ys) = repH xs . repH ys #-}

How do we turn off augument, etc? I suspect (++) is being inlined.

[RyanGlScott]

One possible lead is that GHC's RULES simplifier changed from 7.10.1 to 7.10.2 (apparently due to this commit). The text library was affected due to this change, and their fix was to fire certain RULES in phase 1 of the simplifier.

I tried changing some RULES in various examples' HList.hs files to no avail, so there's probably some internal HERMIT changes needed to properly deal with this.

[andygill]

I suspect that the fix of ticket 10602 is part of the problem we are having.

[andygill]

The first thing (in hermit-shell) we need to fix is getting show-rules and show-rule ported, so we can debug what is going on. I've no idea why repH ++ disappears.

[xich]

Hmmm, it does indeed look like both ++ and . are getting inlined in the rule before it even gets to HERMIT. This looks to be a temporary blip with GHC 7.10.2. According to comments starting here:

https://ghc.haskell.org/trac/ghc/ticket/10528#comment:13

SPJ has already fixed it. (He makes sure that inlining and rule application no longer happens in the LHS of rules.)

Unfortunately, this means HERMIT is pretty much unusable with 7.10.2. I've left a comment on that GHC ticket asking that his fixed be merged and a 7.10.3 released. In the meantime, we need to either target 7.10.1 or build our own 7.10.2 with that patch applied.

To prevent this in the future, perhaps we should track HEAD more closely with our automated tests? It would be nice to catch this sort of thing before it makes it into a release, because (honestly) we aren't important enough to force a GHC patch-level release every time something like this happens.

[RyanGlScott]

In the meantime, we need to either target 7.10.1 or build our own 7.10.2 with that patch applied.

Aw, that's a bummer. I didn't include a GHC HEAD build on Travis before since I had written it off as too unstable, but it looks like we might have seen this bug in time if I had :(

Well, I suppose the only thing we can do now is prevent the use of GHC 7.10.2 to build HERMIT, and add a HEAD build to Travis.

[xich]

I built 7.10.2 with SPJ's patch applied... it sort of fixes the problem. The rules/lemmas apply again like they are supposed to (the LHS is what we would expect again). However, the inlining still appears to be happening on the RHS of the rule/lemma... so the result of the application/rewriting is still different from before. (Nominally, this only makes one test actually fail, as the only difference in all the others is that composition is inlined where it wasn't before, but the scripts still complete successfully.)

I'm going to look around in the GHC code to see if RHSs are still being overly simplified and suggest a patch. Hopefully we can get it merged in time for 7.10.3.

[xich]

Well my patch definitely fixes the HERMIT testsuite (by turning off inlining/rule application in the RHS of rules), but I think SPJ is reluctant to go that route... we'll see, discussion is ongoing on the GHC ticket.

Perhaps its time we work on a concrete syntax for HERMIT lemmas and stop co-opting RULES pragmas? Most of the GHC functionality for parsing/desugaring RULES could just be re-used. I'll look into it.

[andygill]

Let me understand this.

There are two issues
(1) Simplifying the LHS of RULES
(2) Simplifying the RHS of RULES

• 7.10.2 introduced (1), which will be reversed for 7.10.3.
• (2) steps over some definitions, like (.), by unfolding them.

We can not work around (1) without serious hacking, but (2) can be worked around, though is annoying.

Correct?

[xich]

Yes. Though my contention is that (2) was also introduced in 7.10.2 (by the same commit that introduced (1)), and it should not have been.

(1) is a total deal breaker, but thankfully it is fixed and slated to be merged in 7.10.3
(2) is not a total deal breaker... we could just update scripts to work with the new RHSs. However, I'd argue this behavior is unexpected by the user, and makes using HERMIT significantly less natural. For instance, applying rules right-to-left will be significantly harder in many cases because the RHS is simplified.

That the behavior changed is obvious. I'm currently trying to figure out exactly how it changed so I can make a separate ticket about it. Either simplification in the RHS didn't happen before, or it happened during the simplifier pass (which runs after HERMIT). Now it is happening before HERMIT runs (even though it is the first pass).

[ecaustin]

Sorry, I'm trying to catch up now that I'm back in town.

As Drew pointed out, this might be a good impetus for switching to an implementation of lemmas that does not rely on the rules syntax.

In addition avoiding any future changes to the simplifier, it would eliminate the restrictions on the logical forms that our lemmas can take, i.e. we could utilize other logical connectives beyond universal quantification and equality.

The downside of going down this path, at least the biggest one I can see right now, is that we would likely have to implement lemmas using a pre-processor to the HERMIT client, a la SHE.

I say that, because given the push back Drew got in the comments on the GHC ticket, I don't see them being that open to adding a new pragma to GHC that only one, possibly two if I get back to working on HaskHOL, library uses.

[xich]

GHC does have its annotations mechanism... but I think the current implementation of annotations wouldn't be ideal. The annotation payload is required to have Data and Typeable instances, for one. I think we'd get more of a quasi-quote syntax to specifying lemmas rather than the Haskell syntax available to RULES. It is possible we could use them though, and I'd like to at least try it.

Another alternative is to just not embed rules/lemmas in the Haskell source at all, and define them in the HERMIT script. We could essentially create:

define-lemma "foo" "forall xs ys. repH (xs ++ ys) = repH xs . repH ys"

where the string version of the property could be parsed, typechecked, desugared, etc using functions in the GHC API (we have the ability to run all the earlier phases of the compiler, so this is possible to do in the context of the current program, or even in context of the current focus).

In some ways I think that would be preferable, since it keeps lemma definitions in the scripts, where they are used, and out of the source, where they are not. It is also preferable because it doesn't require changes to GHC, or support from GHC devs. But I know at one point in the past @andygill wanted to embed the scripts themselves in the source, to have it all in one file... so its really a design decision.

[ecaustin]

Right, but we could get around the the Data/Typeable issues by storing lemmas as string values annotated at the module level.

If thats the case, then the only significant change would be making sure that HERMIT grabs the annotations from the ModGuts, which it might do already?

[xich]

@roboguy13 Regarding #142 ... definitely a temporary workaround to get the test suite to pass. We need the ability to use rules from other modules (lemmas aside, it is useful to use rules as HERMIT rewrites). However, this is a good thing to know. If the rules are okay when they are in the same module, it means they aren't being simplified before HERMIT gets them (which is what I thought was happening). Maybe its just the case that the simplifier is simplifying them, then the simplified version is being exported in the module interface (or persisting in GHC caches).

@ecaustin Ah yes, we could just store the annotations as strings... good point. Picking up the annotations in HERMIT wouldn't be hard (though I don't think we do it currently). We could insert a special pass at the front of the pipeline that just slurps them up and converts them to lemmas. I wonder if annotations make it into the interface file, or otherwise persist across module boundaries?

[xich]

Alright, #10829 got merged today, and should show up in the 7.10.3 release. I'm leaving this ticket open for now, so I remember to revert #142 and bump the minimum GHC version to 7.10.3 once it is out. I just wanted to put a note here to link to the ticket for archival.

[andygill]

Great work! And with the travis build that @RyanGlScott added, we'll catch problems faster in the future.