Possibly confusing "inaccessible right hand side" with nested `Void`-like type

[amesgen]

trafficstars

(based on a true story)

{-# LANGUAGE NamedFieldPuns #-}

module Test where

data A

data B = B
  { stuff :: !Int,
    morestuff :: !Double,
    a :: !A
  }

data C = C
  { foo :: !Int,
    bar :: !Bool,
    baz :: !B
  }

and consider the function

fff :: C -> Int
fff c = if bar then foo else 0
  where
    C {foo, bar} = c

This results in a warning (since GHC 8.8, see 4th bullet point here)

Test.hs:22:5: warning: [-Woverlapping-patterns]
    Pattern match has inaccessible right hand side
    In a pattern binding: C {foo, bar} = ...
   |
22 |     C {foo, bar} = c
   |     ^^^^^^^^^^^^^^^^

Now imagine that B and A are defined in a completely different place (maybe A and the new field a in B were recently introduced as placeholders) than fff. Then this message gives no direct hints what went wrong, and the problematic nested field isn't even mentioned in fff.

(Also, it is a bit confusing that the right hand side is supposed to be inaccessible)

I find it very nice that GHC can warn about this, but maybe it could give a hint which field is Void-like in this case?

[amesgen]

What makes this particularly confusing without already knowing what's going on is that

fff :: C -> Int
fff c = if bar c then foo c else 0

does not print any warning.

[goldfirere]

Lots of fun things to discuss here! Numbering for easy back-reference.

1. The text of the warning is awfully confusing -- especially when a pattern-binding has a right-hand side that is not what the warning is talking about! I propose Pattern-match will never succeed, which should cover all cases where that warning is currently printed. Or maybe Pattern will never match? Importantly, Pattern will never match is different than Pattern is redundant: a pattern that does not match might do something (like forcing a value) -- it just won't match. This is all very good.

2. You're right that bar and foo, as functions, do not induce warnings. The problem is that the warning is really in the definition of bar and foo, if we think of writing them out as functions. Effectively, they are partial record selectors (very partial). You might find https://github.com/ghc-proposals/ghc-proposals/pull/184 interesting. The ideas there are worthy of resurrection in my opinion; note that the ticket was closed due to lack of activity, not because of rejection. I propose that we don't dwell on foo and bar selectors here -- this is a bigger issue than just an error message text.

3. It would be great if GHC could produce some further information about why a pattern-match is redundant or will never match. After all, it works hard to produce proofs for itself -- it just never tells the user! @sgraf812 is the mastermind behind pattern matches and may be able to opine whether GHC's proofs have any hope of being presentable to users. My hunch is that proofs will (sometimes) be long, and so we may end up with Pass -fprint-pattern-match-proofs to see GHC's reasoning in the error message, or similar.

[sgraf812]

An interesting find!

4. If I run the example, I get the same warning printed twice:

   test7.hs:22:5: warning: [-Woverlapping-patterns]
       Pattern match has inaccessible right hand side
       In a pattern binding: C {foo, bar} = ...
      |
   22 |     C {foo, bar} = c
      |     ^^^^^^^^^^^^^^^^
   
   test7.hs:22:5: warning: [-Woverlapping-patterns]
       Pattern match has inaccessible right hand side
       In a pattern binding: C {foo, bar} = ...
      |
   22 |     C {foo, bar} = c
      |     ^^^^^^^^^^^^^^^^
   

5. Also the source span covers the RHS, which probably contributes to the confusion. It would probably help to only mark the pattern in pattern bindings.

1. The text of the warning is awfully confusing

Yes, I agree. The notion of "inaccessible RHS" doesn't really apply here. Something like Pattern will never match seems better all around and even applies to the scenarios where we currently say "inaccessible RHS". So perhaps Pattern match is impossible (for nice symmetry with Pattern match is redundant)?

2. The problem is that the warning is really in the definition of bar and foo,

Yes. Quick example of such a partial record selector: data T = A{foo::Int} | B{bar::String}). We don't warn about either foo or bar at the moment. Although the problem there is that the record selectors aren't exhaustive (there exists a trace in which calling the selector leads to a crash). In the case above, the record selectors are not exhaustive, but redundant (well, unmatchable); they can never be forced (there exists no trace that calls the selector that doesn't end in a crash/all traces in which the selector is called must lead to a crash). Maybe that's worth a warning? NB: This is actually a property of the data type, not the particular field selector, but it's well in the reach of the pattern-match checker to prove the property (simply pretend to check a function f :: T -> (); f !t = () and see whether the match is impossible).

Once we have the code if foo c then bar c else 0, we can't do much about it in the coverage checker. Catching the divergence requires some kind of strictness analysis in the frontend.

3. It would be great if GHC could produce some further information about why a pattern-match is redundant or will never match.

I agree that it would be great to have such a feature.

Although most of the time it is clear from context why a clause can't match, because there is some prior clause that matched the redundant clause. But here clearly that isn't the case. The reason is rather the type of c; there simply is no inhabitant of C that can have a field of type B, that can have a field of type A.

So I'd hope we can print such a justification, but I'm a bit doubtful. That the field type A is empty is just one in a deep tree of ultimately failing inhabitation tests.

Maybe it is always the last failing test that we are interested in? But the checker could also (unsuccessfully) check a ~ _|_ after it established that there are no constructors that B's field a can be instantiated to. Or it could say that b ~ _|_ couldn't be satisfied, although we are really interested in the case when we try to instantiate b ~ B stuff morestuff a and then fail. Is a message such as "b is a strict field and could not be instantiated" really helpful?

Perhaps it's always the failing leaves of the "proof tree" that we are interested in. But as the preceding paragraph demonstrates, that tree can be huge. Maybe display the leaf with the maximum depth?

In a way, it's the same problem as asking an SMT solver for the proof of a property it has proven. It's much easier for it to give counter-examples (e.g., when proving inexhaustivity) than deciding which parts of the proof are relevant or whether it is the simplest such proof...

[Ericson2314]

If I may shift the goal posts a bit, I think the solution is absurd patterns (or rather "absurd alternative") as discussed in https://github.com/ghc-proposals/ghc-proposals/discussions/423

The reason it is so hard to come up with a way to demonstrate why something is partial is because we don't have a syntax for it! But with absurd patterns perhaps we could print out something like

fff :: C -> Int
fff c = if bar then foo else 0
  where
    C { foo, bar, baz = B { a = _ } } = c

as an equivalent program, explaining how its equivalent because baz and a are strict by definition.

The one gotcha I am now reasoning is that https://github.com/ghc-proposals/ghc-proposals/discussions/423 was just talking about pattern matches for functions. Absurd pattern binds, especially in a non-strict language, are harder to think about.