From 56705da84a8e954d9755270ca8bb37a43d7d03a9 Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sebastian.graf@kit.edu>
Date: Sun, 7 Nov 2021 13:09:06 +0100
Subject: [PATCH] Pmc: Do inhabitation test for unlifted vars (#20631)
Although I thought we were already set to handle unlifted datatypes correctly,
it appears we weren't. #20631 showed that it's wrong to assume
`vi_bot=IsNotBot` for `VarInfo`s of unlifted types from their inception if we
don't follow up with an inhabitation test to see if there are any habitable
constructors left. We can't trigger the test from `emptyVarInfo`, so now we
instead fail early in `addBotCt` for variables of unlifted types.
Fixed #20631.
---
compiler/GHC/HsToCore/Pmc/Solver.hs | 41 ++++++++++++-------
compiler/GHC/HsToCore/Pmc/Solver/Types.hs | 6 ++-
.../tests/pmcheck/should_compile/T20631.hs | 24 +++++++++++
testsuite/tests/pmcheck/should_compile/all.T | 2 +
4 files changed, 56 insertions(+), 17 deletions(-)
create mode 100644 testsuite/tests/pmcheck/should_compile/T20631.hs
diff --git a/compiler/GHC/HsToCore/Pmc/Solver.hs b/compiler/GHC/HsToCore/Pmc/Solver.hs
index aafac1451600..41d6eb5ea204 100644
--- a/compiler/GHC/HsToCore/Pmc/Solver.hs
+++ b/compiler/GHC/HsToCore/Pmc/Solver.hs
@@ -560,7 +560,7 @@ data PhiCt
-- ^ @PhiConCt x K tvs dicts ys@ encodes @K \@tvs dicts ys <- x@, matching @x@
-- against the 'PmAltCon' application @K \@tvs dicts ys@, binding @tvs@,
-- @dicts@ and possibly unlifted fields @ys@ in the process.
- -- See Note [Strict fields and fields of unlifted type].
+ -- See Note [Strict fields and variables of unlifted type].
| PhiNotConCt !Id !PmAltCon
-- ^ @PhiNotConCt x K@ encodes "x ≠K", asserting that @x@ can't be headed
-- by @K@.
@@ -685,9 +685,13 @@ addBotCt nabla@MkNabla{ nabla_tm_st = ts@TmSt{ ts_facts=env } } x = do
case bot of
IsNotBot -> mzero -- There was x ≠⊥. Contradiction!
IsBot -> pure nabla -- There already is x ~ ⊥. Nothing left to do
- MaybeBot -> do -- We add x ~ ⊥
- let vi' = vi{ vi_bot = IsBot }
- pure nabla{ nabla_tm_st = ts{ts_facts = addToUSDFM env y vi' } }
+ MaybeBot -> -- We add x ~ ⊥
+ -- Case (3) in Note [Strict fields and variables of unlifted type]
+ if isUnliftedType (idType x)
+ then mzero -- unlifted vars can never be ⊥
+ else do
+ let vi' = vi{ vi_bot = IsBot }
+ pure nabla{ nabla_tm_st = ts{ts_facts = addToUSDFM env y vi' } }
-- | Adds the constraint @x ~/ ⊥@ to 'Nabla'. Quite similar to 'addNotConCt',
-- but only cares for the ⊥ "constructor".
@@ -1102,12 +1106,12 @@ storing required arguments along with the PmAltConLike in 'vi_neg'.
Note [Strict fields and variables of unlifted type]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Binders of unlifted type (and strict fields) are unlifted by construction;
-they are conceived with an implicit @â‰âŠ¥@ constraint to begin with. Hence,
-desugaring in "GHC.HsToCore.Pmc" is entirely unconcerned by strict fields,
-since the forcing happens *before* pattern matching.
-And the φ constructor constraints emitted by 'GHC.HsToCore.Pmc.checkGrd'
-have complex binding semantics (binding type constraints and unlifted fields),
-so unliftedness semantics are entirely confined to the oracle.
+they are conceived with an implicit (but delayed checked) @â‰âŠ¥@ constraint to
+begin with. Hence, desugaring in "GHC.HsToCore.Pmc" is entirely unconcerned
+by strict fields, since the forcing happens *before* pattern matching. And
+the φ constructor constraints emitted by 'GHC.HsToCore.Pmc.checkGrd' have
+complex binding semantics (binding type constraints and unlifted fields), so
+unliftedness semantics are entirely confined to the oracle.
These are the moving parts:
@@ -1138,11 +1142,18 @@ These are the moving parts:
constructor constraint.
3. The preceding points handle unlifted constructor fields, but there also
- are regular binders of unlifted type.
- Since the oracle as implemented has no notion of scoping and bindings,
- we can't know *when* an unlifted variable comes into scope. But that's
- not actually a problem, because we can just add the @x ≠⊥@ to the
- 'emptyVarInfo' when we first encounter it.
+ are regular binders of unlifted type. We simply fail in 'addBotCt' for
+ any binder of unlifted type.
+ It would be enough to check for unliftedness once, when the binder comes
+ into scope, but we haven't really a way to track that.
+
+ 4. Why not start an 'emptyVarInfo' of unlifted type with @vi_bot = IsNotBot@?
+ Because then we'd need to trigger an inhabitation test, because the var
+ might actually be void to begin with. But we can't trigger the test from
+ 'emptyVarInfo'.
+ Historically, that is what we did and not doing the test led to #20631,
+ where 'addNotBotCt' trivially succeeded, because the 'VarInfo' already
+ said 'IsNotBot', implying that a prior inhabitation test succeeded.
-}
-------------------------
diff --git a/compiler/GHC/HsToCore/Pmc/Solver/Types.hs b/compiler/GHC/HsToCore/Pmc/Solver/Types.hs
index 1fcaf44a4fd2..d60233569210 100644
--- a/compiler/GHC/HsToCore/Pmc/Solver/Types.hs
+++ b/compiler/GHC/HsToCore/Pmc/Solver/Types.hs
@@ -291,9 +291,11 @@ emptyVarInfo x
{ vi_id = x
, vi_pos = []
, vi_neg = emptyPmAltConSet
- -- Case (3) in Note [Strict fields and fields of unlifted type]
+ -- Why not set IsNotBot for unlifted type here?
+ -- Because we'd have to trigger an inhabitation test, which we can't.
+ -- See case (4) in Note [Strict fields and variables of unlifted type]
-- in GHC.HsToCore.Pmc.Solver
- , vi_bot = if isUnliftedType (idType x) then IsNotBot else MaybeBot
+ , vi_bot = MaybeBot
, vi_rcm = emptyRCM
}
diff --git a/testsuite/tests/pmcheck/should_compile/T20631.hs b/testsuite/tests/pmcheck/should_compile/T20631.hs
new file mode 100644
index 000000000000..d255c521ba97
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T20631.hs
@@ -0,0 +1,24 @@
+{-# LANGUAGE UnliftedDatatypes #-}
+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+module Lib where
+import Data.Kind (Type)
+import GHC.Exts (UnliftedType)
+
+type Foo :: UnliftedType -> Type -> Type
+data Foo a b =
+ Bar a -- no need for strictness annotation
+ | Baz b
+
+type MyVoid :: UnliftedType
+data MyVoid
+
+v :: Foo MyVoid Char
+v = Baz 'c'
+
+main :: IO ()
+main = case v of
+ -- The Baz case is impossible
+ -- MyVoid has no values, and it can't
+ -- be undefined because it's unlifted.
+ Baz c -> putChar c
+
diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index c732ef5691c2..f1cc928151f2 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/testsuite/tests/pmcheck/should_compile/all.T
@@ -168,6 +168,8 @@ test('T18932', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T19622', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T20631', normal, compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
# Other tests
test('pmc001', [], compile,
--
GitLab