A bug in exprIsHNF

Introduction

The function exprIsHNF checks whether a given CoreExpr is in head normal form. It uses the exprIsHNFlike to do the bulk of the work, which in turn is defined in terms of is_hnf_like which is where the bug is.

The particular buggy code path is when it checks if an application is in head normal form.

Running Example

As a running example we can take the example listed in a comment in this function:

f (x /# y)
-- where f has arity two

As a comment explains, usually partially applied functions are in HNF, but in this case the unboxed argument still needs evaluation, so f (x /# y) is not in HNF and exprIsHNF should return False.

The Bug

The relevant case of is_hnf_like is:

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

Our running example matches this case with [e :-> f] and [a :-> x /# y]. The code checks isValArg (x /# y) which returns True (isValArg simply checks that its argument is not a type). So, we take the app_is_value f 1 case.

This is the bug, we throw away the a, or in the running example x /# y!

The relevant case of app_is_value is:

app_is_value (Var f)    nva = id_app_is_value f nva

So in the running example it will continue with id_app_is_value f 1.

And id_app_is_value is defined as:

    id_app_is_value id n_val_args
       = is_con id
       || idArity id > n_val_args

In the running example f is not a constructor and its arity is 2, so this ends up checking 2 > 1 which is True, not False as we expected!

The Solution

What needs to happen instead? The app_is_value function does have the required logic in the case for App (and that is also where the comment about f (x /# y) is):

    app_is_value (App f a)  nva
      | isValArg a              =
        app_is_value f (nva + 1) &&
        not (needsCaseBinding (exprType a) a)
          -- For example  f (x /# y)  where f has arity two, and the first
          -- argument is unboxed. This is not a value!
          -- But  f 34#  is a value.
          -- NB: Check app_is_value first, the arity check is cheaper

A quick fix then would be to change the App case of is_hnf_expr to:

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

But in light of !10841 (comment 517254) I think there is more we need to do here around constructors with strict fields.