'let' getting changed into 'case' in a RULE

[roboguy13]

I have a RULE:

{-# RULES "abs/let-float" [~]
    forall x v.
    abs (let bnd = v in x)
      =
    let bnd = v
    in
    abs x
  #-}

When I try to bring it into a lemma with rule-to-lemma (or look at it with show-rule), it "becomes":

abs/let-float (Not Proven)
  ∀ △ △ $dLift $d~ x v.
  abs ▲ $dLift $d~
      (case v of bnd ▲
         _ → x)
  ≡
  case HEq_sc ▲ ▲ ▲ ▲ ($p1~ ▲ ▲ ▲ $d~) of cobox ▲
    _ →
      case v of bnd ▲
        _ → abs ▲ $dLift (($d~ ▹ (■ ∷ ▲ ~R ▲)) ▹ (■ ∷ ▲ ~R ▲)) x

I imagine this is something GHC is doing, not HERMIT. As a result of this (I think), I cannot apply it where I would like to (where there is a let, not a case). I know that case and let have different semantics in Core with regard to strictness, so I imagine this is why I can't apply it in those places.

Is there a way around this or a way to tell it to keep it as let?

[xich]

Yes, this is GHC enforcing the let/app invariant:

https://github.com/ghc/ghc/blob/68f72f101d67b276aff567be03619a3fd9618017/compiler/coreSyn/CoreSyn.hs#L355

It is because the let is built with mkCoreLets:

https://downloads.haskell.org/~ghc/latest/docs/html/libraries/ghc-8.0.1/MkCore.html#v:mkCoreLets

Your best bet is probably to build the lemma directly, instead of via a rule. You could define your own library, e.g.

https://github.com/ku-fpg/hermit-reasoning-14/blob/master/Reasoning-with-the-HERMIT/MakingACentury/hermit-century-lemmas/HERMIT/Libraries/Century.hs

The appendix of the reasoning paper sort of explains what is going on there:

http://ku-fpg.github.io/files/Farmer-15-HERMIT-reasoning.pdf

[xich]

FWIW, mkLets will build let expressions without enforcing the invariant:

https://downloads.haskell.org/~ghc/latest/docs/html/libraries/ghc-8.0.1/CoreSyn.html#v:mkLets