| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
-------------------------
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The `PmExprEq` business was a huge hack and was at the same time vastly
too powerful and not powerful enough to encode negative term equalities,
i.e. facts of the form "forall y. x ≁ Just y".
This patch introduces the concept of 'refutable shapes': What matters
for the pattern match checker is being able to encode knowledge of the
kind "x can no longer be the literal 5". We encode this knowledge in a
`PmRefutEnv`, mapping a set of newly introduced `PmAltCon`s (which are
just `PmLit`s at the moment) to each variable denoting above
inequalities.
So, say we have `x ≁ 42 ∈ refuts` in the term oracle context and
try to solve an equality like `x ~ 42`. The entry in the refutable
environment will immediately lead to a contradiction.
This machinery renders the whole `PmExprEq` and `ComplexEq` business
unnecessary, getting rid of a lot of (mostly dead) code.
See the Note [Refutable shapes] in TmOracle for a place to start.
Metric Decrease:
T11195
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Issues #16289 and #15713 are proof that the pattern match checker did
an unsound job of estimating the value set abstraction corresponding to
the uncovered set.
The reason is that the fix from #11303 introducing `NLit` was
incomplete: The `LitCon` case desugared to `Var` rather than `LitVar`,
which would have done the necessary case splitting analogous to the
`ConVar` case.
This patch rectifies that by introducing the fresh unification variable
in `LitCon` in value abstraction position rather than pattern postition,
recording a constraint equating it to the constructor expression rather
than the literal. Fixes #16289 and #15713.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This switches the compiler/ component to get compiled with
-XNoImplicitPrelude and a `import GhcPrelude` is inserted in all
modules.
This is motivated by the upcoming "Prelude" re-export of
`Semigroup((<>))` which would cause lots of name clashes in every
modulewhich imports also `Outputable`
Reviewers: austin, goldfire, bgamari, alanz, simonmar
Reviewed By: bgamari
Subscribers: goldfire, rwbarton, thomie, mpickering, bgamari
Differential Revision: https://phabricator.haskell.org/D3989
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
Eliminate ListSetOps from imp_trust_pkgs and imp_dep_pkgs
Replace Map with NameEnv in TmOracle
Reviewers: austin, dfeuer, bgamari
Reviewed By: bgamari
Subscribers: thomie
Differential Revision: https://phabricator.haskell.org/D3113
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This patch adds a new pragma so that users can specify `COMPLETE` sets of
`ConLike`s in order to sate the pattern match checker.
A function which matches on all the patterns in a complete grouping
will not cause the exhaustiveness checker to emit warnings.
```
pattern P :: ()
pattern P = ()
{-# COMPLETE P #-}
foo P = ()
```
This example would previously have caused the checker to warn that
all cases were not matched even though matching on `P` is sufficient to
make `foo` covering. With the addition of the pragma, the compiler
will recognise that matching on `P` alone is enough and not emit
any warnings.
Reviewers: goldfire, gkaracha, alanz, austin, bgamari
Reviewed By: alanz
Subscribers: lelf, nomeata, gkaracha, thomie
Differential Revision: https://phabricator.haskell.org/D2669
GHC Trac Issues: #8779
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Overhaul the Overhauled Pattern Match Checker
* Changed the representation of Value Set Abstractions. Instead of
using a prefix tree, we now use a list of Value Vector Abstractions.
The set of constraints Delta for every Value Vector Abstraction is the
oracle state so that we solve everything only once.
* Instead of doing everything lazily, we prune at once (and in general
everything is much stricter). Hence, an example written with pattern
guards is checked in almost the same time as the equivalent with
pattern matching.
* Do not store the covered and the divergent sets at all. Since what we
only need is a yes/no (does this clause cover anything? Does it force
any thunk?) We just keep a boolean for each.
* Removed flags `-Wtoo-many-guards` and `-ffull-guard-reasoning`.
Replaced with `fmax-pmcheck-iterations=n`. Still debatable what should
the default `n` be.
* When a guard is for sure not going to contribute anything, we treat
it as such: The oracle is not called and cases `CGuard`, `UGuard` and
`DGuard` from the paper are not happening at all (the generation of a
fresh variable, the unfolding of the pattern list etc.). his combined
with the above seems to be enough to drop the memory increase for test
T783 down to 18.7%.
* Do not export function `dsPmWarn` (it is now called directly from
within `checkSingle` and `checkMatches`).
* Make `PmExprVar` hold a `Name` instead of an `Id`. The term oracle
does not handle type information so using `Id` was a waste of
time/space.
* Added testcases T11195, T11303b (data families) and T11374
The patch addresses at least the following:
Trac #11195, #11276, #11303, #11374, #11162
Test Plan: validate
Reviewers: goldfire, bgamari, hvr, austin
Subscribers: simonpj, thomie
Differential Revision: https://phabricator.haskell.org/D1795
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Two changes:
1. Instead of generating constraints of the form (x ~ e) (as we do in
the paper), generate constraints of the form (e ~ e). The term oracle
(`tmOracle` in deSugar/TmOracle.hs) is not really efficient and in the
presence of many (x ~ e) constraints behaves quadratically. For
literals, constraints of the form (False ~ (x ~ lit)) are pretty common,
so if we start with { y ~ False, y ~ (x ~ lit) } we end up givng to the
solver (a) twice as many constraints as we need and (b) half of them
trigger the solver's weakness. This fixes #11160.
2. Treat two overloaded literals that look different as different. This
is not entirely correct but it is what both the previous and the current
check did. I had the ambitious plan to do the *right thing* (equality
between overloaded literals is undecidable in the general case) and just
use this assumption when issuing the warnings. It seems to generate much
more constraints than I expected (breaks #11161) so I just do it
immediately now instead of generating everything and filtering
afterwards.
Even if it is not (strictly speaking) correct, we have the following:
* Gives the "expected" warnings (the ones Ocaml or the previous
algorithm would give) and,
* Most importantly, it is safe. Unless a catch-all clause exists, a
match against literals is always non-exhaustive. So, effectively
this affects only what is shown to the user (and, evidently,
performance!).
|
|
|
This patch adresses several problems concerned with exhaustiveness and
redundancy checking of pattern matching. The list of improvements includes:
* Making the check type-aware (handles GADTs, Type Families, DataKinds, etc.).
This fixes #4139, #3927, #8970 and other related tickets.
* Making the check laziness-aware. Cases that are overlapped but affect
evaluation are issued now with "Patterns have inaccessible right hand side".
Additionally, "Patterns are overlapped" is now replaced by "Patterns are
redundant".
* Improved messages for literals. This addresses tickets #5724, #2204, etc.
* Improved reasoning concerning cases where simple and overloaded
patterns are matched (See #322).
* Substantially improved reasoning for pattern guards. Addresses #3078.
* OverloadedLists extension does not break exhaustiveness checking anymore
(addresses #9951). Note that in general this cannot be handled but if we know
that an argument has type '[a]', we treat it as a list since, the instance of
'IsList' gives the identity for both 'fromList' and 'toList'. If the type is
not clear or is not the list type, then the check cannot do much still. I am
a bit concerned about OverlappingInstances though, since one may override the
'[a]' instance with e.g. an '[Int]' instance that is not the identity.
* Improved reasoning for nested pattern matching (partial solution). Now we
propagate type and (some) term constraints deeper when checking, so we can
detect more inconsistencies. For example, this is needed for #4139.
I am still not satisfied with several things but I would like to address at
least the following before the next release:
Term constraints are too many and not printed for non-exhaustive matches
(with the exception of literals). This sometimes results in two identical (in
appearance) uncovered warnings. Unless we actually show their difference, I
would like to have a single warning.
|
