TmOracle: Replace negative term equalities by refutable PmAltCons
authorSebastian Graf <sebastian.graf@kit.edu>
Wed, 22 May 2019 16:46:37 +0000 (18:46 +0200)
committerMarge Bot <ben+marge-bot@smart-cactus.org>
Fri, 7 Jun 2019 14:21:21 +0000 (10:21 -0400)
commite963beb54a243f011396942d2add644e3f3dd8ae
tree169670dd67cafacf288d0cd0fd68b560dd51797f
parentd3915b304f297b8a2534f6abf9c2984837792921
TmOracle: Replace negative term equalities by refutable PmAltCons

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
15 files changed:
compiler/basicTypes/NameEnv.hs
compiler/deSugar/Check.hs
compiler/deSugar/DsMonad.hs
compiler/deSugar/PmExpr.hs
compiler/deSugar/PmPpr.hs [new file with mode: 0644]
compiler/deSugar/TmOracle.hs
compiler/ghc.cabal.in
compiler/typecheck/TcEvidence.hs
compiler/typecheck/TcRnTypes.hs
compiler/utils/ListSetOps.hs
testsuite/tests/pmcheck/should_compile/CyclicSubst.hs [new file with mode: 0644]
testsuite/tests/pmcheck/should_compile/PmExprVars.hs [new file with mode: 0644]
testsuite/tests/pmcheck/should_compile/T12949.hs [new file with mode: 0644]
testsuite/tests/pmcheck/should_compile/all.T
testsuite/tests/typecheck/should_compile/T5490.stderr