Opened 3 years ago

Last modified 4 months ago

#13021 new bug

Inaccessible RHS warning is confusing for users

Reported by: mpickering Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.0.1
Keywords: PatternMatchWarnings Cc: gkaracha
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

The pattern match checker makes the distinction between redundant matches and matches with an inaccessible right hand side.

A pattern with an inaccessible RHS, is a redundant pattern which forces the argument so affects strictness.

I think this is confusing for users as most of the time you write programs assuming totality but the error message doesn't make it clear why the two warnings are different. I think that instead they should both be called redundant but a note added to the inaccessible case explaining that removing it could affect strictness.

Change History (11)

comment:1 Changed 3 years ago by gkaracha

Even though I understand that the message can be confusing, I disagree with calling it in any way "redundant". Pattern matching is side-effectful in a lazy language and in fact we often use it just to force evaluation, so I would not consider it a minor thing. Before GHC 8, both redundant and with-inaccessible-rhs clauses where called "overlapping" which may be more appropriate.

comment:2 Changed 3 years ago by goldfire

I'm with @gkaracha here in that I would want these messages to remain separate.

On the other hand, I'd love it if we could put URLs in error messages (perhaps enabled by a -fprint-info-links flag or some such) so that confused users can get more information.

comment:3 Changed 3 years ago by mpickering

How is a user expected to react to this warning? It seems that they can't act on it without changing the semantics of their program.

comment:4 Changed 3 years ago by goldfire

Do you have an example that we could contemplate?

comment:5 Changed 3 years ago by mpickering

It is easy to trigger cases like this with COMPLETE signatures as they are currently designed.

For example,

data T = A | B | C

{-# COMPLETE B #-}

foo :: T -> ()
foo A = ()
foo B = ()

Then the first match is reported as having an inaccessible RHS.

comment:6 Changed 3 years ago by gkaracha

Yes, it makes sense in these cases, since they are actually semantically wrong. But is there an example for a meaningful COMPLETE set?

comment:7 Changed 3 years ago by rwbarton

I don't understand what is going on in this example. Suppose B was a pattern synonym and we couldn't see its definition. Then the COMPLETE pragma could be semantically correct. But if we match A before B then the match isn't redundant, the behavior of the function could be different in the A case.

comment:8 Changed 3 years ago by mpickering

The COMPLETE pragma is an assertion that writing a function which matches on each of the constructors in the set is total. In this example, for this to be true, there can be no A values as if there were, no function just matching on B would be total. Thus, the warning about the inaccessible RHS is correct wrt the assertion made by the programmer.

comment:9 Changed 3 years ago by rwbarton

My confusion here is at a very basic level. _ is a pattern such that any set of pattern matches which includes _ is total. Yet in a function like

f :: Maybe a -> Int
f Nothing = 0
f _ = 1

the first equation is not redundant in a practical sense, even though the pattern match would still be total without it. There's more to life than totality of pattern matches.

I thought that a {-# COMPLETE p1, ..., pn #-} pragma was just supposed to mean that a function that matches all of the pi should be regarded as total. It doesn't make any sense to me for the compiler to use this knowledge plus the definitions of the pi to make any conclusions about whether other values are possible or not.

comment:10 Changed 3 years ago by goldfire

I'm with @rwbarton. The fact that B is COMPLETE in comment:5 does not make the first match redundant or inaccessible. His suggestion to consider pattern B <- _ (which is indeed a complete pattern) is instructive.

comment:11 Changed 4 months ago by Marge Bot <ben+marge-bot@…>

In 7915afc/ghc:

Encode shape information in `PmOracle`

Previously, we had an elaborate mechanism for selecting the warnings to
generate in the presence of different `COMPLETE` matching groups that,
albeit finely-tuned, produced wrong results from an end user's
perspective in some cases (#13363).

The underlying issue is that at the point where the `ConVar` case has to
commit to a particular `COMPLETE` group, there's not enough information
to do so and the status quo was to just enumerate all possible complete
sets nondeterministically.  The `getResult` function would then pick the
outcome according to metrics defined in accordance to the user's guide.
But crucially, it lacked knowledge about the order in which affected
clauses appear, leading to the surprising behavior in #13363.

In !1010 we taught the term oracle to reason about literal values a
variable can certainly not take on. This MR extends that idea to
`ConLike`s and thereby fixes #13363: Instead of committing to a
particular `COMPLETE` group in the `ConVar` case, we now split off the
matching constructor incrementally and record the newly covered case as
a refutable shape in the oracle. Whenever the set of refutable shapes
covers any `COMPLETE` set, the oracle recognises vacuosity of the
uncovered set.

This patch goes a step further: Since at this point the information
in value abstractions is merely a cut down representation of what the
oracle knows, value abstractions degenerate to a single `Id`, the
semantics of which is determined by the oracle state `Delta`.
Value vectors become lists of `[Id]` given meaning to by a single
`Delta`, value set abstractions (of which the uncovered set is an
instance) correspond to a union of `Delta`s which instantiate the
same `[Id]` (akin to models of formula).

Fixes #11528 #13021, #13363, #13965, #14059, #14253, #14851, #15753, #17096, #17149

-------------------------
Metric Decrease:
    ManyAlternatives
    T11195
-------------------------
Note: See TracTickets for help on using tickets.