1. 26 Sep, 2020 1 commit
  2. 24 Sep, 2020 1 commit
  3. 22 Sep, 2020 1 commit
    • Sebastian Graf's avatar
      PmCheck: Rewrite inhabitation test · e9501547
      Sebastian Graf authored
      We used to produce inhabitants of a pattern-match refinement type Nabla
      in the checker in at least two different and mostly redundant ways:
        1. There was `provideEvidence` (now called
           `generateInhabitingPatterns`) which is used by
           `GHC.HsToCore.PmCheck` to produce non-exhaustive patterns, which
           produces inhabitants of a Nabla as a sub-refinement type where all
           match variables are instantiated.
        2. There also was `ensure{,All}Inhabited` (now called
           `inhabitationTest`) which worked slightly different, but was
           whenever new type constraints or negative term constraints were
           added. See below why `provideEvidence` and `ensureAllInhabited`
           can't be the same function, the main reason being performance.
        3. And last but not least there was the `nonVoid` test, which tested
           that a given type was inhabited. We did use this for strict fields
           and -XEmptyCase in the past.
      The overlap of (3) with (2) was always a major pet peeve of ...
  4. 13 Sep, 2020 1 commit
    • Sebastian Graf's avatar
      Make `tcCheckSatisfiability` incremental (#18645) · 69ea2fee
      Sebastian Graf authored
      By taking and returning an `InertSet`.
      Every new `TcS` session can then pick up where a prior session left with
      Since we don't want to unflatten the Givens (and because it leads to
      infinite loops, see !3971), we introduced a new variant of `runTcS`,
      `runTcSInerts`, that takes and returns the `InertSet` and makes
      sure not to unflatten the Givens after running the `TcS` action.
      Fixes #18645 and #17836.
      Metric Decrease:
  5. 12 Sep, 2020 1 commit
    • Sebastian Graf's avatar
      PmCheck: Disattach COMPLETE pragma lookup from TyCons · 2a942285
      Sebastian Graf authored
      By not attaching COMPLETE pragmas with a particular TyCon and instead
      assume that every COMPLETE pragma is applicable everywhere, we can
      drastically simplify the logic that tries to initialise available
      COMPLETE sets of a variable during the pattern-match checking process,
      as well as fixing a few bugs.
      Of course, we have to make sure not to report any of the
      ill-typed/unrelated COMPLETE sets, which came up in a few regression
      In doing so, we fix #17207, #18277 and #14422.
      There was a metric decrease in #18478 by ~20%.
      Metric Decrease:
  6. 10 Sep, 2020 2 commits
    • Sebastian Graf's avatar
      PmCheck: Handle ⊥ and strict fields correctly (#18341) · 3777be14
      Sebastian Graf authored
      In #18341, we discovered an incorrect digression from Lower Your Guards.
      This MR changes what's necessary to support properly fixing #18341.
      In particular, bottomness constraints are now properly tracked in the
      oracle/inhabitation testing, as an additional field
      `vi_bot :: Maybe Bool` in `VarInfo`. That in turn allows us to
      model newtypes as advertised in the Appendix of LYG and fix #17725.
      Proper handling of ⊥ also fixes #17977 (once again) and fixes #18670.
      For some reason I couldn't follow, this also fixes #18273.
      I also added a couple of regression tests that were missing. Most of
      them were already fixed before.
      In summary, this patch fixes #18341, #17725, #18273, #17977 and #18670.
      Metric Decrease:
    • Sebastian Graf's avatar
      Add long-distance info for pattern bindings (#18572) · 67ce72da
      Sebastian Graf authored
      We didn't consider the RHS of a pattern-binding before, which led to
      surprising warnings listed in #18572.
      As can be seen from the regression test T18572, we get the expected
      output now.
  7. 19 Aug, 2020 1 commit
    • Alex D's avatar
      Implement -Wredundant-bang-patterns (#17340) · 731c8d3b
      Alex D authored
      Add new flag '-Wredundant-bang-patterns' that enables checks for "dead" bangs.
      Dead bangs are the ones that under no circumstances can force a thunk that
      wasn't already forced. Dead bangs are a form of redundant bangs. The new check
      is performed in Pattern-Match Coverage Checker along with other checks (namely,
      redundant and inaccessible RHSs). Given
          f :: Bool -> Int
          f True = 1
          f !x   = 2
      we can detect dead bang patterns by checking whether @x ~ ⊥@ is satisfiable
      where the PmBang appears in 'checkGrdTree'. If not, then clearly the bang is
      dead. Such a dead bang is then indicated in the annotated pattern-match tree by
      a 'RedundantSrcBang' wrapping. In 'redundantAndInaccessibles', we collect
      all dead bangs to warn about.
      Note that we don't want to warn for a dead bang that appears on a redundant
      clause. That is because in that case, we recommend to delete the clause wholly,
      including its leading pattern match.
      Dead bang patterns are redundant. But there are bang patterns which are
      redundant that aren't dead, for example
          f !() = 0
      the bang still forces the match variable, before we attempt to match on (). But
      it is redundant with the forcing done by the () match. We currently don't
      detect redundant bangs that aren't dead.
  8. 13 Aug, 2020 1 commit
    • Sebastian Graf's avatar
      PmCheck: Better long-distance info for where bindings (#18533) · 55dec4dc
      Sebastian Graf authored
      Where bindings can see evidence from the pattern match of the `GRHSs`
      they belong to, but not from anything in any of the guards (which belong
      to one of possibly many RHSs).
      Before this patch, we did *not* consider said evidence, causing #18533,
      where the lack of considering type information from a case pattern match
      leads to failure to resolve the vanilla COMPLETE set of a data type.
      Making available that information required a medium amount of
      refactoring so that `checkMatches` can return a
      `[(Deltas, NonEmpty Deltas)]`; one `(Deltas, NonEmpty Deltas)` for each
      `GRHSs` of the match group. The first component of the pair is the
      covered set of the pattern, the second component is one covered set per
      Fixes #18533.
      Regression test case: T18533
  9. 23 Jul, 2020 1 commit
    • Sebastian Graf's avatar
      Add regression test for #18478 · 02f40b0d
      Sebastian Graf authored
      !3392 backported !2993 to GHC 8.10.2 which most probably is responsible
      for fixing #18478, which triggered a pattern match checker performance
      regression in GHC 8.10.1 as first observed in #17977.
  10. 01 May, 2020 1 commit
    • Sebastian Graf's avatar
      PmCheck: Pick up `EvVar`s bound in `HsWrapper`s for long-distance info · fd7ea0fe
      Sebastian Graf authored
      `HsWrapper`s introduce evidence bindings through `WpEvLam` which the
      pattern-match coverage checker should be made aware of.
      Failing to do so caused #18049, where the resulting impreciseness of
      imcompleteness warnings seemingly contradicted with
      The solution is simple: Collect all the evidence binders of an
      `HsWrapper` and add it to the ambient `Deltas` before desugaring
      the wrapped expression.
      But that means we pick up many more evidence bindings, even when they
      wrap around code without a single pattern match to check! That regressed
      `T3064` by over 300%, so now we are adding long-distance info lazily
      through judicious use of `unsafeInterleaveIO`.
      Fixes #18049.
  11. 01 Apr, 2020 1 commit
    • Sebastian Graf's avatar
      PmCheck: Adjust recursion depth for inhabitation test · 7b217179
      Sebastian Graf authored
      In #17977, we ran into the reduction depth limit of the typechecker.
      That was only a symptom of a much broader issue: The recursion depth
      of the coverage checker for trying to instantiate strict fields in the
      `nonVoid` test was far too high (100, the `defaultMaxTcBound`).
      As a result, we were performing quite poorly on `T17977`.
      Short of a proper termination analysis to prove emptyness of a type,
      we just arbitrarily default to a much lower recursion limit of 3.
      Fixes #17977.
  12. 27 Feb, 2020 1 commit
    • Sebastian Graf's avatar
      PmCheck: Implement Long-distance information with Covered sets · 74311e10
      Sebastian Graf authored
      data T = A | B | C
      f :: T -> Int
      f A = 1
      f x = case x of
        A -> 2
        B -> 3
        C -> 4
      Clearly, the RHS returning 2 is redundant. But we don't currently see
      that, because our approximation to the covered set of the inner case
      expression just picks up the positive information from surrounding
      pattern matches. It lacks the context sensivity that `x` can't be `A`
      Therefore, we adopt the conceptually and practically superior approach
      of reusing the covered set of a particular GRHS from an outer pattern
      match. In this case, we begin checking the `case` expression with the
      covered set of `f`s second clause, which encodes the information that
      `x` can't be `A` anymore. After this MR, we will successfully warn about
      the RHS returning 2 being redundant.
      Perhaps surprisingly, this was a great simplification to the code of
      both the coverage checker and the desugarer.
      Found a redundant case alternative in `unix` submodule, so we have to
      bump it with a fix.
      Metric Decrease:
  13. 11 Feb, 2020 1 commit
    • Sebastian Graf's avatar
      Fix long distance info for record updates · f3e737bb
      Sebastian Graf authored
      For record updates where the `record_expr` is a variable, as in #17783:
      data PartialRec = No
                      | Yes { a :: Int, b :: Bool }
      update No = No
      update r@(Yes {}) = r { b = False }
      We should make use of long distance info in
      `-Wincomplete-record-updates` checking. But the call to `matchWrapper`
      in the `RecUpd` case didn't specify a scrutinee expression, which would
      correspond to the `record_expr` `r` here. That is fixed now.
      Fixes #17783.
  14. 05 Feb, 2020 1 commit
    • Sebastian Graf's avatar
      PmCheck: Record type constraints arising from existentials in `PmCoreCt`s · c90eca55
      Sebastian Graf authored
      In #17703 (a follow-up of !2192), we established that contrary to my
      belief, type constraints arising from existentials in code like
      data Ex where Ex :: a -> Ex
      f _ | let x = Ex @Int 15 = case x of Ex -> ...
      are in fact useful.
      This commit makes a number of refactorings and improvements to comments,
      but fundamentally changes `addCoreCt.core_expr` to record the type
      constraint `a ~ Int` in addition to `x ~ Ex @a y` and `y ~ 15`.
      Fixes #17703.
  15. 25 Jan, 2020 1 commit
    • Sebastian Graf's avatar
      PmCheck: Formulate as translation between Clause Trees · 8038cbd9
      Sebastian Graf authored
      We used to check `GrdVec`s arising from multiple clauses and guards in
      isolation. That resulted in a split between `pmCheck` and
      `pmCheckGuards`, the implementations of which were similar, but subtly
      different in detail. Also the throttling mechanism described in
      `Note [Countering exponential blowup]` ultimately got quite complicated
      because it had to cater for both checking functions.
      This patch realises that pattern match checking doesn't just consider
      single guarded RHSs, but that it's always a whole set of clauses, each
      of which can have multiple guarded RHSs in turn. We do so by
      translating a list of `Match`es to a `GrdTree`:
      data GrdTree
        = Rhs !RhsInfo
        | Guard !PmGrd !GrdTree      -- captures lef-to-right  match semantics
        | Sequence !GrdTree !GrdTree -- captures top-to-bottom match semantics
        | Empty                      -- For -XEmptyCase, neutral element of Sequence
      Then we have a function `checkGrdTree` that matches a given `GrdTree`
      against an incoming set of values, represented by `Deltas`:
      checkGrdTree :: GrdTree -> Deltas -> CheckResult
      Throttling is isolated to the `Sequence` case and becomes as easy as one
      would expect: When the union of uncovered values becomes too big, just
      return the original incoming `Deltas` instead (which is always a
      superset of the union, thus a sound approximation).
      The returned `CheckResult` contains two things:
      1. The set of values that were not covered by any of the clauses, for
         exhaustivity warnings.
      2. The `AnnotatedTree` that enriches the syntactic structure of the
         input program with divergence and inaccessibility information.
      This is `AnnotatedTree`:
      data AnnotatedTree
        = AccessibleRhs !RhsInfo
        | InaccessibleRhs !RhsInfo
        | MayDiverge !AnnotatedTree
        | SequenceAnn !AnnotatedTree !AnnotatedTree
        | EmptyAnn
      Crucially, `MayDiverge` asserts that the tree may force diverging
      values, so not all of its wrapped clauses can be redundant.
      While the set of uncovered values can be used to generate the missing
      equations for warning messages, redundant and proper inaccessible
      equations can be extracted from `AnnotatedTree` by
      For this to work properly, the interface to the Oracle had to change.
      There's only `addPmCts` now, which takes a bag of `PmCt`s. There's a
      whole bunch of `PmCt` variants to replace the different oracle functions
      from before.
      The new `AnnotatedTree` structure allows for more accurate warning
      reporting (as evidenced by a number of changes spread throughout GHC's
      code base), thus we fix #17465.
      Fixes #17646 on the go.
      Metric Decrease:
  16. 05 Nov, 2019 1 commit
    • Sebastian Graf's avatar
      Check EmptyCase by simply adding a non-void constraint · 1593debf
      Sebastian Graf authored
      We can handle non-void constraints since !1733, so we can now express
      the strictness of `-XEmptyCase` just by adding a non-void constraint
      to the initial Uncovered set.
      For `case x of {}` we thus check that the Uncovered set `{ x | x /~ ⊥ }`
      is non-empty. This is conceptually simpler than the plan outlined in
       #17376, because it talks to the oracle directly.
      In order for this patch to pass the testsuite, I had to fix handling of
      newtypes in the pattern-match checker (#17248).
      Since we use a different code path (well, the main code path) for
      `-XEmptyCase` now, we apparently also handle #13717 correctly.
      There's also some dead code that we can get rid off now.
      `provideEvidence` has been updated to provide output more in line with
      the old logic, which used `inhabitationCandidates` under the hood.
      A consequence of the shift away from the `UncoveredPatterns` type is
      that we don't report reduced type families for empty case matches,
      because the pretty printer is pure and only knows the match variable's
      Fixes #13717, #17248, #17386
  17. 12 Oct, 2019 1 commit
    • Sebastian Graf's avatar
      Much simpler language for PmCheck · 30f5ac07
      Sebastian Graf authored
      Simon realised that the simple language composed of let bindings, bang
      patterns and flat constructor patterns is enough to capture the
      semantics of the source pattern language that are important for
      pattern-match checking. Well, given that the Oracle is smart enough to
      connect the dots in this less informationally dense form, which it is
      So we transform `translatePat` to return a list of `PmGrd`s relative to
      an incoming match variable. `pmCheck` then trivially translates each of
      the `PmGrd`s into constraints that the oracle understands.
      Since we pass in the match variable, we incidentally fix #15884
      (coverage checks for view patterns) through an interaction with !1746.
  18. 08 Oct, 2019 1 commit
    • Sebastian Graf's avatar
      PmCheck: Look up parent data family TyCon when populating `PossibleMatches` · f691f0c2
      Sebastian Graf authored
      The vanilla COMPLETE set is attached to the representation TyCon of a
      data family instance, whereas the user-defined COMPLETE sets are
      attached to the parent data family TyCon itself.
      Previously, we weren't trying particularly hard to get back to the
      representation TyCon to the parent data family TyCon, resulting in bugs
      like #17207. Now we should do much better.
      Fixes the original issue in #17207, but I found another related bug that
      isn't so easy to fix.
  19. 01 Oct, 2019 2 commits
  20. 28 Sep, 2019 1 commit
    • Sebastian Graf's avatar
      PmCheck: No ConLike instantiation in pmcheck · c5d888d4
      Sebastian Graf authored
      `pmcheck` used to call `refineToAltCon` which would refine the knowledge
      we had about a variable by equating it to a `ConLike` application.
      Since we weren't particularly smart about this in the Check module, we
      simply freshened the constructors existential and term binders utimately
      through a call to `mkOneConFull`.
      But that instantiation is unnecessary for when we match against a
      concrete pattern! The pattern will already have fresh binders and field
      types. So we don't call `refineToAltCon` from `Check` anymore.
      Subsequently, we can simplify a couple of call sites and functions in
      `PmOracle`. Also implementing `computeCovered` becomes viable and we
      don't have to live with the hack that was `addVarPatVecCt` anymore.
      A side-effect of not indirectly calling `mkOneConFull` anymore is that
      we don't generate the proper strict argument field constraints anymore.
      Instead we now desugar ConPatOuts as if they had bangs on their strict
      fields. This implies that `PmVar` now carries a `HsImplBang` that we
      need to respect by a (somewhat ephemeral) non-void check. We fix #17234
      in doing so.
  21. 25 Sep, 2019 1 commit
    • Sebastian Graf's avatar
      PmCheck: Only ever check constantly many models against a single pattern · ebc65025
      Sebastian Graf authored
      Introduces a new flag `-fmax-pmcheck-deltas` to achieve that. Deprecates
      the old `-fmax-pmcheck-iter` mechanism in favor of this new flag.
      From the user's guide:
      Pattern match checking can be exponential in some cases. This limit makes sure
      we scale polynomially in the number of patterns, by forgetting refined
      information gained from a partially successful match. For example, when
      matching `x` against `Just 4`, we split each incoming matching model into two
      sub-models: One where `x` is not `Nothing` and one where `x` is `Just y` but
      `y` is not `4`. When the number of incoming models exceeds the limit, we
      continue checking the next clause with the original, unrefined model.
      This also retires the incredibly hard to understand "maximum number of
      refinements" mechanism, because the current mechanism is more general
      and should catch the same exponential cases like PrelRules at the same
      Metric Decrease:
  22. 19 Sep, 2019 1 commit
  23. 16 Sep, 2019 1 commit
    • Sebastian Graf's avatar
      Encode shape information in `PmOracle` · 7915afc6
      Sebastian Graf authored
      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:
  24. 28 Aug, 2019 1 commit
    • Sebastian Graf's avatar
      Fix #17112 · a308b435
      Sebastian Graf authored
      The `mkOneConFull` function of the pattern match checker used to try to
      guess the type arguments of the data type's type constructor by looking
      at the ambient type of the match. This doesn't work well for Pattern
      Synonyms, where the result type isn't even necessarily a TyCon
      application, and it shows in #11336 and #17112.
      Also the effort seems futile; why try to try hard when the type checker
      has already done the hard lifting? After this patch, we instead supply
      the type constructors arguments as an argument to the function and
      lean on the type-annotated AST.
  25. 07 Jun, 2019 1 commit
    • Sebastian Graf's avatar
      TmOracle: Replace negative term equalities by refutable PmAltCons · e963beb5
      Sebastian Graf authored
      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
      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:
  26. 08 Apr, 2019 1 commit
    • Sebastian Graf's avatar
      Make `singleConstructor` cope with pattern synonyms · d236d9d0
      Sebastian Graf authored
      Previously, `singleConstructor` didn't handle singleton `COMPLETE` sets
      of a single pattern synonym, resulting in incomplete pattern warnings
      in #15753.
      This is fixed by making `singleConstructor` (now named
      `singleMatchConstructor`) query `allCompleteMatches`, necessarily making
      it effectful. As a result, most of this patch is concerned with
      threading the side-effect through to `singleMatchConstructor`.
      Unfortunately, this is not enough to completely fix the original
      reproduction from #15753 and #15884, which are related to function
      applications in pattern guards being translated too conservatively.
  27. 03 Apr, 2019 1 commit
    • Sebastian Graf's avatar
      Fix Uncovered set of literal patterns · 4626cf21
      Sebastian Graf authored
      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.
  28. 07 Nov, 2018 1 commit
    • davide's avatar
      testsuite: Save performance metrics in git notes. · 932cd41d
      davide authored
      This patch makes the following improvement:
        - Automatically records test metrics (per test environment) so that
          the programmer need not supply nor update expected values in *.T
          - On expected metric changes, the programmer need only indicate the
            direction of change in the git commit message.
        - Provides a simple python tool "perf_notes.py" to compare metrics
          over time.
        - Using just the previous commit allows performance to drift with each
          - Currently we allow drift as we have a preference for minimizing
            false positives.
          - Some possible alternatives include:
            - Use metrics from a fixed commit per test: the last commit that
              allowed a change in performance (else the oldest metric)
            - Or use some sort of aggregate since the last commit that allowed
              a change in performance (else all available metrics)
            - These alternatives may result in a performance issue (with the
              test driver) having to heavily search git commits/notes.
        - Run locally, performance tests will trivially pass unless the tests
          were run locally on the previous commit. This is often not the case
          e.g.  after pulling recent changes.
      Previously, *.T files contain statements such as:
      stats_num_field('peak_megabytes_allocated', (2, 1))
      compiler_stats_num_field('bytes allocated',
                               [(wordsize(64), 165890392, 10)])
      This required the programmer to give the expected values and a tolerance
      deviation (percentage). With this patch, the above statements are
      replaced with:
      collect_stats('peak_megabytes_allocated', 5)
      collect_compiler_stats('bytes allocated', 10)
      So that programmer must only enter which metrics to test and a tolerance
      deviation. No expected value is required. CircleCI will then run the
      tests per test environment and record the metrics to a git note for that
      commit and push them to the git.haskell.org ghc repo. Metrics will be
      compared to the previous commit. If they are different by the tolerance
      deviation from the *.T file, then the corresponding test will fail. By
      adding to the git commit message e.g.
       # Metric (In|De)crease <metric(s)> <options>: <tests>
      Metric Increase ['bytes allocated', 'peak_megabytes_allocated'] \
               (test_env='linux_x86', way='default'):
          Test012, Test345
      Metric Decrease 'bytes allocated':
      Metric Increase:
      This will allow the noted changes (letting the test pass). Note that by
      omitting metrics or options, the change will apply to all possible
      metrics/options (i.e. in the above, an increase for all metrics in all
      test environments is allowed for Test711)
      phabricator will use the message in the description
      Reviewers: bgamari, hvr
      Reviewed By: bgamari
      Subscribers: rwbarton, carter
      GHC Trac Issues: #12758
      Differential Revision: https://phabricator.haskell.org/D5059
  29. 28 Sep, 2018 1 commit
    • Ryan Scott's avatar
      Normalise EmptyCase types using the constraint solver · e72d7880
      Ryan Scott authored
      Certain `EmptyCase` expressions were mistakently producing
      warnings since their types did not have as many type families reduced
      as they could have. The most direct way to fix this is to normalise
      these types initially using the constraint solver to solve for any
      local equalities that may be in scope.
      Test Plan: make test TEST=T14813
      Reviewers: simonpj, bgamari, goldfire
      Reviewed By: simonpj
      Subscribers: rwbarton, carter
      GHC Trac Issues: #14813
      Differential Revision: https://phabricator.haskell.org/D5094
  30. 23 Sep, 2018 1 commit
    • Ryan Scott's avatar
      Add a recursivity check in nonVoid · e68b439f
      Ryan Scott authored
      Previously `nonVoid` outright refused to call itself
      recursively to avoid the risk of hitting infinite loops when
      checking recurisve types. But this is too conservative—we //can//
      call `nonVoid` recursively as long as we incorporate a way to detect
      the presence of recursive types, and bail out if we do detect one.
      Happily, such a mechanism already exists in the form of `checkRecTc`,
      so let's use it.
      Test Plan: make test TEST=T15584
      Reviewers: simonpj, bgamari
      Reviewed By: simonpj
      Subscribers: rwbarton, carter
      GHC Trac Issues: #15584
      Differential Revision: https://phabricator.haskell.org/D5116
  31. 27 Aug, 2018 1 commit
    • Ryan Scott's avatar
      Take strict fields into account in coverage checking · 744b034d
      Ryan Scott authored
      The current pattern-match coverage checker implements the
      formalism presented in the //GADTs Meet Their Match// paper in a
      fairly faithful matter. However, it was discovered recently that
      there is a class of unreachable patterns that
      //GADTs Meet Their Match// does not handle: unreachable code due to
      strict argument types, as demonstrated in #15305. This patch
      therefore goes off-script a little and implements an extension to
      the formalism presented in the paper to handle this case.
      Essentially, when determining if each constructor can be matched on,
      GHC checks if its associated term and type constraints are
      satisfiable. This patch introduces a new form of constraint,
      `NonVoid(ty)`, and checks if each constructor's strict argument types
      satisfy `NonVoid`. If any of them do not, then that constructor is
      deemed uninhabitable, and thus cannot be matched on. For the full
      story of how this works, see
      `Note [Extensions to GADTs Meet Their Match]`.
      Along the way, I did a little bit of much-needed refactoring. In
      particular, several functions in `Check` were passing a triple of
      `(ValAbs, ComplexEq, Bag EvVar)` around to represent a constructor
      and its constraints. Now that we're adding yet another form of
      constraint to the mix, I thought it appropriate to turn this into
      a proper data type, which I call `InhabitationCandidate`.
      Test Plan: make test TEST=T15305
      Reviewers: simonpj, bgamari
      Reviewed By: simonpj
      Subscribers: rwbarton, carter
      GHC Trac Issues: #15305
      Differential Revision: https://phabricator.haskell.org/D5087
  32. 01 Aug, 2018 1 commit
    • Ryan Scott's avatar
      Fix #15450 by refactoring checkEmptyCase' · 7f3cb50d
      Ryan Scott authored
      `checkEmptyCase'` (the code path for coverage-checking
      `EmptyCase` expressions) had a fair bit of code duplication from the
      code path for coverage-checking non-`EmptyCase` expressions, and to
      make things worse, it behaved subtly different in some respects (for
      instance, emitting different warnings under unsatisfiable
      constraints, as shown in #15450). This patch attempts to clean up
      both this discrepancy and the code duplication by doing the
      * Factor out a `pmInitialTmTyCs` function, which returns the initial
        set of term and type constraints to use when beginning coverage
        checking. If either set of constraints is unsatisfiable, we use an
        empty set in its place so that we can continue to emit as many
        warnings as possible. (The code path for non-`EmptyCase`
        expressions was doing this already, but not the code path for
        `EmptyCase` expressions, which is the root cause of #15450.)
        Along the way, I added a `Note` to explain why we do this.
      * Factor out a `pmIsSatisfiable` constraint which checks if a set of
        term and type constraints are satisfiable. This does not change any
        existing behavior; this is just for the sake of deduplicating code.
      Test Plan: make test TEST=T15450
      Reviewers: simonpj, bgamari
      Subscribers: rwbarton, thomie, carter
      GHC Trac Issues: #15450
      Differential Revision: https://phabricator.haskell.org/D5017
  33. 30 Jul, 2018 1 commit
    • Ryan Scott's avatar
      Fix #15385 by using addDictsDs in matchGuards · 9d388eb8
      Ryan Scott authored
      When coverage checking pattern-matches, we rely on the call
      sites in the desugarer to populate the local dictionaries and term
      evidence in scope using `addDictsDs` and `addTmCsDs`. But it turns
      out that only the call site for desugaring `case` expressions was
      actually doing this properly. In another part of the desugarer,
      `matchGuards` (which handles pattern guards), it did not update the
      local dictionaries in scope at all, leading to #15385.
      Fixing this is relatively straightforward: just augment the
      `BindStmt` case of `matchGuards` to use `addDictsDs` and `addTmCsDs`.
      Accomplishing this took a little bit of import/export tweaking:
      * We now need to export `collectEvVarsPat` from `HsPat.hs`.
      * To avoid an import cycle with `Check.hs`, I moved `isTrueLHsExpr`
        from `DsGRHSs.hs` to `DsUtils.hs`, which resides lower on the
        import chain.
      Test Plan: make test TEST=T15385
      Reviewers: simonpj, bgamari
      Reviewed By: simonpj
      Subscribers: rwbarton, thomie, carter
      GHC Trac Issues: #15385
      Differential Revision: https://phabricator.haskell.org/D4968
  34. 15 Jul, 2018 1 commit
  35. 02 Mar, 2018 1 commit
    • Ryan Scott's avatar
      Fix the coverage checker's treatment of existential tyvars · a2d03c69
      Ryan Scott authored
      Previously, the pattern-match coverage checker was far too
      eager to freshen the names of existentially quantified type
      variables, which led to incorrect sets of type constraints that
      misled GHC into thinking that certain programs that involve nested
      GADT pattern matches were non-exhaustive (when in fact they were).
      Now, we generate extra equality constraints in the ConCon case of
      the coverage algorithm to ensure that these fresh tyvars align
      with existing existential tyvars. See
      `Note [Coverage checking and existential tyvars]` for the full story.
      Test Plan: make test TEST="T11984 T14098"
      Reviewers: gkaracha, bgamari, simonpj
      Reviewed By: simonpj
      Subscribers: simonpj, rwbarton, thomie, carter
      GHC Trac Issues: #11984, #14098
      Differential Revision: https://phabricator.haskell.org/D4434
  36. 05 Aug, 2017 1 commit
    • Ryan Scott's avatar
      Don't warn when empty casing on Type · a267580e
      Ryan Scott authored
      `Type` (a.k.a. `TYPE LiftedRep`) can be used at the type level thanks
      to `TypeInType`. However, expressions like
      f :: Type -> Int
      f x = case x of {}
      were falsely claiming that the empty case on the value of type `Type` was
      non-exhaustive. The reason is a bit silly: `TYPE` is technically not an empty
      datatype in GHC's eyes, since it's a builtin, primitive type. To convince the
      pattern coverage checker otherwise, this adds a special case for `TYPE`.
      Test Plan: make test TEST=T14086
      Reviewers: gkaracha, austin, bgamari, goldfire
      Reviewed By: goldfire
      Subscribers: goldfire, rwbarton, thomie
      GHC Trac Issues: #14086
      Differential Revision: https://phabricator.haskell.org/D3819
  37. 21 Apr, 2017 1 commit
  38. 04 Apr, 2017 1 commit