diff options
| -rw-r--r-- | compiler/GHC/HsToCore/Pmc/Solver.hs | 41 | ||||
| -rw-r--r-- | compiler/GHC/HsToCore/Pmc/Solver/Types.hs | 6 | ||||
| -rw-r--r-- | testsuite/tests/pmcheck/should_compile/T20631.hs | 24 | ||||
| -rw-r--r-- | testsuite/tests/pmcheck/should_compile/all.T | 2 |
4 files changed, 56 insertions, 17 deletions
diff --git a/compiler/GHC/HsToCore/Pmc/Solver.hs b/compiler/GHC/HsToCore/Pmc/Solver.hs index aafac14516..41d6eb5ea2 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 1fcaf44a4f..d602335692 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 0000000000..d255c521ba --- /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 c732ef5691..f1cc928151 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, |