Bug in exprIsHNF

Consider

{-# LANGUAGE MagicHash #-}

module Foo where

import GHC.Exts

f1 :: a -> Int# -> Int -> Int
{-# OPAQUE f1 #-}
f1 _ x (I# y) = I# (x +# y)

f2 :: Int# -> a -> Int -> Int
{-# OPAQUE f2 #-}
f2 x _ (I# y) = I# (x +# y)

loopy :: Int -> Int#
loopy x | x>0       = loopy x
        | otherwise = 0#

foo x = let t :: Int -> Int
            t = f1 True (loopy x) in   -- or   f2 (loopy x) True
        t `seq` (x, t)

You would expect this program to behave the same whether we call f1 or f2 in foo; they differ only in the order of arguments. And yet:

-- Calling f1:
foo
  = \ (x_aKa :: Int) ->
      (x_aKa, f1 @Bool GHC.Types.True (loopy x_aKa))

-- Calling f2
foo
  = \ (x_aKa :: Int) ->
      case f2 @Bool (loopy x_aKa) GHC.Types.True of t_aKb { __DEFAULT ->
      (x_aKa, t_aKb)
      }

Bonkers!

Diagnosis

There is a bug in GHC.Core.Utils.exprIsHNFlike:

    is_hnf_like (App e a)
      | isValArg a               = app_is_value e 1
      | otherwise                = is_hnf_like e

This totally ignores what a is like. But

    app_is_value (App f a)  nva
      | isValArg a              =
        app_is_value f (nva + 1) &&
        not (needsCaseBinding (exprType a) a)

For subsequent argument we do the needsCaseBinding thing, correctly.