Skip to content
  • Sebastian Graf's avatar
    Check EmptyCase by simply adding a non-void constraint · 1593debf
    Sebastian Graf authored and Marge Bot's avatar Marge Bot committed
    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
    type.
    
    Fixes #13717, #17248, #17386
    1593debf