error "This argument does not satisfy the let/app invariant"

[ninegua]

This is with hermit version 1.0.1 and GHC 7.10.3 on Linux. Program is simple:

x = 2 :: Integer
y = 1 / fromIntegral x :: Double

main = print y

I ran the follow hermit session:

hermit test.hs
[starting HERMIT v1.0.1 on test.hs]
% ghc test.hs -fforce-recomp -O2 -dcore-lint -fsimple-list-literals -fexpose-all-unfoldings -fplugin=HERMIT -fplugin-opt=HERMIT:*:
[1 of 1] Compiling Main             ( test.hs, test.o )
module Main where
  y ∷ Double
  main ∷ IO ()
  main ∷ IO ()
hermit<0> rhs-of 'y
(/) ▲ $fFractionalDouble (D# 1.0) (fromIntegral ▲ ▲ $fIntegralInteger $fNumDouble (__integer 2))
hermit<1> repeat (any-bu specialize >>> bash)
case doubleFromInteger (__integer 2) of wild ▲
  _ →
    case (/##) 1.0 (doubleFromInteger (__integer 2)) of wild2 ▲
      _ → D# wild2
hermit<2>
*** Core Lint errors : in result of Core plugin:  HERMIT0 ***
<no location info>: Warning:
    In the expression: /## 1.0 (doubleFromInteger (__integer 2))
    This argument does not satisfy the let/app invariant:
      doubleFromInteger (__integer 2)
*** Offending Program ***
y :: Double
[LclId, Str=DmdType]
y =
  case doubleFromInteger (__integer 2) of _ [Occ=Dead] { __DEFAULT ->
  case /## 1.0 (doubleFromInteger (__integer 2))
  of wild2_a1q9 { __DEFAULT ->
  D# wild2_a1q9
  }
  }

main :: IO ()
[LclIdX, Str=DmdType]
main = print @ Double $fShowDouble y

main :: IO ()
[LclIdX, Str=DmdType]
main = runMainIO @ () main

*** End of Offense ***


<no location info>:
Compilation had errors

Is it related to issue #139? Does changing GHC version help?

[andygill]

Thanks. We'll look into this.

[ninegua]

It turns out if

  D# ((/##) 1.0 (doubleFromInteger (__integer 2)))

is rewritten as:

  case case doubleFromInteger (__integer 2) of w' ▲
         _ → (/##) 1.0 w'
   of z' ▲
    _ → D# z'

Then lint will succeed. But doing so manually is rather tiresome. I tried the following with the above program, and it works (not sure about the smash part in the proof, but whatever works!)

rhs-of 'y
repeat ((any-bu specialize) >>> smash)
application-of 'doubleFromInteger
{ let-intro 'z; let-body; case-intro-seq 'z; case-expr; inline 'z; up; up; let-elim }
up
case-float-arg-lemma A
-- recording obligations as lemmas : A
smash
end-proof -- proven A
{ let-intro 'z; let-body; case-intro-seq 'z; case-expr; inline 'z; up; up; let-elim }
up
case-float-arg-lemma B
-- recording obligations as lemmas : B
smash
end-proof -- proven B
up

Turning the "troubled" arg into case was relatively straightforward, but since there are two levels of nested application (/##) and D#, case-float-arg has to be done twice.

Would appreciate if there is a more automatic way to fix this kind of error, or better yet if we can avoid violating the let/app rule in case elimination in the first place.

[xich]

Given: https://github.com/ghc/ghc/blob/master/compiler/coreSyn/CoreSyn.hs#L375

My guess is that some rewrite is building the application with an explicit App constructor rather than using the mkCoreApp smart constructor.

Can you narrow down when exactly that expression gets built?

[ninegua]

Here is a log after I set-auto-corelint True and use bash-debug:

...
[case-reduce (before)]
case D# (doubleFromInteger (__integer 2)) of wild1 ▲
  D# y →
    case (/##) 1.0 y of wild2 ▲
      _ → D# wild2
[case-reduce (after)]
case (/##) 1.0 (doubleFromInteger (__integer 2)) of wild2 ▲
  _ → D# wild2
<1> <no location info>: Warning:
    In the expression: /## 1.0 (doubleFromInteger (__integer 2))
    This argument does not satisfy the let/app invariant:
      doubleFromInteger (__integer 2)
Error in expression: repeat ((any-bu specialize) >>> bash-debug)
Core Lint Failed:
<no location info>: Warning:
    In the expression: /## 1.0 (doubleFromInteger (__integer 2))
    This argument does not satisfy the let/app invariant:
      doubleFromInteger (__integer 2)

The issue seems to be a result of using substExpr in the implementation of caseReduceDataconR. So a valid App f x becomes invalid because x is substituted. Not sure what is the best way to guard this. Maybe rule out the situation when the "substitutee" is of an unboxed type?