1. 26 Jan, 2017 1 commit
    • Matthew Pickering's avatar
      COMPLETE pragmas for enhanced pattern exhaustiveness checking · 1a3f1eeb
      Matthew Pickering authored
      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
      1a3f1eeb
  2. 04 Feb, 2016 1 commit
    • Georgios Karachalias's avatar
      Overhaul the Overhauled Pattern Match Checker · 28f951ed
      Georgios Karachalias authored
      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
      28f951ed
  3. 05 Dec, 2015 2 commits
  4. 04 Dec, 2015 2 commits
    • Georgios Karachalias's avatar
      99d01e1d
    • Georgios Karachalias's avatar
      Improve performance for PM check on literals (Fixes #11160 and #11161) · ae4398d6
      Georgios Karachalias authored
      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!).
      ae4398d6
  5. 03 Dec, 2015 1 commit
    • Georgios Karachalias's avatar
      Major Overhaul of Pattern Match Checking (Fixes #595) · 8a506104
      Georgios Karachalias authored
      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.
      8a506104