[Git][ghc/ghc][wip/T18341] 7 commits: Add regression test for #18341
Sebastian Graf
gitlab at gitlab.haskell.org
Fri Jul 3 14:06:13 UTC 2020
Sebastian Graf pushed to branch wip/T18341 at Glasgow Haskell Compiler / GHC
Commits:
b5848d19 by Sebastian Graf at 2020-07-02T16:06:13+02:00
Add regression test for #18341
- - - - -
65cfd0cd by Sebastian Graf at 2020-07-02T16:09:34+02:00
Add regression test for #17725
- - - - -
9cc7c0e7 by Sebastian Graf at 2020-07-02T16:37:03+02:00
Add regression test for #17378
- - - - -
1555fcbd by Sebastian Graf at 2020-07-02T17:14:48+02:00
Add regression test for #10183
- - - - -
a275c6f1 by Sebastian Graf at 2020-07-02T17:16:15+02:00
Add regression test for #17729
- - - - -
a3fe3572 by Sebastian Graf at 2020-07-02T17:29:41+02:00
Add regression test for fixed #18273
- - - - -
6f30cf6b by Sebastian Graf at 2020-07-03T16:06:06+02:00
Refactor ensureInhabited and resolve a scoping bug from the previous refactor
- - - - -
12 changed files:
- compiler/GHC/HsToCore/PmCheck.hs
- compiler/GHC/HsToCore/PmCheck/Oracle.hs
- + testsuite/tests/pmcheck/should_compile/T10183.hs
- + testsuite/tests/pmcheck/should_compile/T17378.hs
- + testsuite/tests/pmcheck/should_compile/T17725.hs
- + testsuite/tests/pmcheck/should_compile/T17725.stderr
- + testsuite/tests/pmcheck/should_compile/T17729.hs
- + testsuite/tests/pmcheck/should_compile/T17729.stderr
- + testsuite/tests/pmcheck/should_compile/T18273.hs
- + testsuite/tests/pmcheck/should_compile/T18341.hs
- + testsuite/tests/pmcheck/should_compile/T18341.stderr
- testsuite/tests/pmcheck/should_compile/all.T
Changes:
=====================================
compiler/GHC/HsToCore/PmCheck.hs
=====================================
@@ -1005,8 +1005,8 @@ checkGrdTree' (Guard (PmBang x) tree) deltas = do
checkGrdTree' (Guard (PmCon x con tvs dicts args) tree) deltas = do
unc_this <- addPmCtDeltas deltas (PmNotConCt x con)
let cts = pmConCts x con tvs dicts args
- tracePm "check:Con" (ppr cts)
deltas' <- addPmCtsDeltas deltas cts
+ tracePm "check:Con" (ppr cts)
CheckResult tree' unc_inner prec <- checkGrdTree' tree deltas'
limit <- maxPmCheckModels <$> getDynFlags
let (prec', unc') = throttle limit deltas (unc_this Semi.<> unc_inner)
@@ -1018,6 +1018,7 @@ checkGrdTree' (Guard (PmCon x con tvs dicts args) tree) deltas = do
checkGrdTree' (Sequence l r) unc_0 = do
tracePm "check:Sequence:l" (ppr l)
CheckResult l' unc_1 prec_l <- checkGrdTree' l unc_0
+ tracePm "check:Sequence:r" (ppr r)
CheckResult r' unc_2 prec_r <- checkGrdTree' r unc_1
pure CheckResult
{ cr_clauses = SequenceAnn l' r'
=====================================
compiler/GHC/HsToCore/PmCheck/Oracle.hs
=====================================
@@ -1015,42 +1015,44 @@ ensureInhabited :: Delta -> VarInfo -> DsM (Maybe VarInfo)
-- NB: Does /not/ filter each ConLikeSet with the oracle; members may
-- remain that do not statisfy it. This lazy approach just
-- avoids doing unnecessary work.
-ensureInhabited _ vi at VI{ vi_bot = Nothing } = pure (Just vi)
-ensureInhabited _ vi at VI{ vi_bot = Just True } = pure (Just vi)
-ensureInhabited delta vi = do
- vi <- initPossibleMatches (delta_ty_st delta) vi
- fmap (set_cache vi) <$> test (vi_cache vi)
+ensureInhabited delta vi = case vi_bot vi of
+ Nothing -> pure (Just vi) -- The |-Bot rule from the paper
+ Just True -> pure (Just vi)
+ Just False -> initPossibleMatches (delta_ty_st delta) vi >>= inst_complete_sets
where
- set_cache vi cache = vi { vi_cache = cache }
-
- test NoPM = pure (Just NoPM)
- test (PM ms) = runMaybeT (PM <$> traverse one_set ms)
-
- one_set cs = find_one_inh cs (uniqDSetToList cs)
-
- find_one_inh :: ConLikeSet -> [ConLike] -> MaybeT DsM ConLikeSet
- -- (find_one_inh cs cls) iterates over cls, deleting from cs
+ -- | This is the |-Inst rule from the paper (section 4.5). Tries to
+ -- find an inhabitant in every complete set by instantiating with one their
+ -- constructors. If there is any complete set where we can't find an
+ -- inhabitant, the whole thing is uninhabited.
+ inst_complete_sets :: VarInfo -> DsM (Maybe VarInfo)
+ inst_complete_sets vi at VI{ vi_cache = NoPM } = pure (Just vi)
+ inst_complete_sets vi at VI{ vi_cache = PM ms } = runMaybeT $ do
+ ms <- traverse (\cs -> inst_complete_set vi cs (uniqDSetToList cs)) ms
+ pure vi{ vi_cache = PM ms }
+
+ inst_complete_set :: VarInfo -> ConLikeSet -> [ConLike] -> MaybeT DsM ConLikeSet
+ -- (inst_complete_set cs cls) iterates over cls, deleting from cs
-- any uninhabited elements of cls. Stop (returning Just cs)
-- when you see an inhabited element; return Nothing if all
-- are uninhabited
- find_one_inh _ [] = mzero
- find_one_inh cs (con:cons) = lift (inh_test con) >>= \case
+ inst_complete_set _ _ [] = mzero
+ inst_complete_set vi cs (con:cons) = lift (inst_and_test vi con) >>= \case
True -> pure cs
- False -> find_one_inh (delOneFromUniqDSet cs con) cons
+ False -> inst_complete_set vi (delOneFromUniqDSet cs con) cons
- inh_test :: ConLike -> DsM Bool
- -- @inh_test K@ Returns False if a non-bottom value @v::ty@ cannot possibly
+ inst_and_test :: VarInfo -> ConLike -> DsM Bool
+ -- @inst_and_test K@ Returns False if a non-bottom value @v::ty@ cannot possibly
-- be of form @K _ _ _ at . Returning True is always sound.
--
-- It's like 'DataCon.dataConCannotMatch', but more clever because it takes
-- the facts in Delta into account.
- inh_test con = do
+ inst_and_test vi con = do
env <- dsGetFamInstEnvs
case guessConLikeUnivTyArgsFromResTy env (vi_ty vi) con of
Nothing -> pure True -- be conservative about this
Just arg_tys -> do
(_tvs, _vars, ty_cs, strict_arg_tys) <- mkOneConFull arg_tys con
- tracePm "inh_test" (ppr con $$ ppr ty_cs)
+ tracePm "inst_and_test" (ppr con $$ ppr ty_cs)
-- No need to run the term oracle compared to pmIsSatisfiable
fmap isJust <$> runSatisfiabilityCheck delta $ mconcat
-- Important to pass False to tyIsSatisfiable here, so that we won't
=====================================
testsuite/tests/pmcheck/should_compile/T10183.hs
=====================================
@@ -0,0 +1,22 @@
+{-# LANGUAGE GADTs, DataKinds, TypeOperators, UnicodeSyntax #-}
+
+module Foo where
+
+import GHC.TypeLits
+
+data List l t where
+ Nil ∷ List 0 t
+ (:-) ∷ t → List l t → List (l+1) t
+
+head' ∷ (1<=l) ⇒ List l t → t
+head' (x :- _) = x
+
+data T a where
+ TT :: T Bool
+ TF :: T Int
+
+f :: T Bool -> Bool
+f TT = True
+
+g :: (a ~ Bool) => T a -> Bool
+g TT = True
=====================================
testsuite/tests/pmcheck/should_compile/T17378.hs
=====================================
@@ -0,0 +1,30 @@
+{-# OPTIONS_GHC -Wincomplete-patterns -fforce-recomp #-}
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE EmptyCase #-}
+module Lib where
+
+import Data.Type.Equality
+import Data.Functor.Identity
+import Data.Void
+
+f :: a :~: Int -> a :~: Bool -> ()
+f !_ x = case x of {}
+
+g :: Identity (a :~: Int) -> a :~: Bool -> ()
+g (Identity _) Refl = ()
+
+data SMaybe a = SNothing
+ | SJust !a
+
+-- | Exhaustive. Note how in addition to @{(a,b) | b /~ True}@, the value set
+-- @{(a,b) | y /~ SNothing, b ~ True}@ flows into the next equation, but @y@ is
+-- no longer in scope. Normally, we have no way of matching on that without a
+-- wildcard match, but in this case we refute @y ~ SJust z@ by unleashing type
+-- evidence saying that @z@ must be 'Void' by matching on 'Void'.
+h :: forall a. a :~: Void -> Bool -> ()
+h _ True | let y = undefined :: SMaybe a, SNothing <- y = ()
+h Refl False = ()
=====================================
testsuite/tests/pmcheck/should_compile/T17725.hs
=====================================
@@ -0,0 +1,10 @@
+{-# OPTIONS_GHC -Wincomplete-patterns -fforce-recomp #-}
+{-# LANGUAGE BangPatterns #-}
+module Lib where
+
+newtype IInt = IInt Int
+
+f :: IInt -> Bool -> ()
+f !(IInt _) True = ()
+f (IInt 42) True = ()
+f _ _ = ()
=====================================
testsuite/tests/pmcheck/should_compile/T17725.stderr
=====================================
@@ -0,0 +1,4 @@
+
+T17725.hs:9:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+ Pattern match is redundant
+ In an equation for ‘f’: f (IInt 42) True = ...
=====================================
testsuite/tests/pmcheck/should_compile/T17729.hs
=====================================
@@ -0,0 +1,13 @@
+{-# LANGUAGE PatternSynonyms #-}
+{-# OPTIONS_GHC -fforce-recomp -Wincomplete-patterns #-}
+
+incomplete :: Maybe a -> Bool
+incomplete ma = case (ma, ()) of
+ (Nothing, _) -> False
+
+{-# COMPLETE Pat #-}
+pattern Pat :: a -> b -> (a, b)
+pattern Pat a b = (a, b)
+
+main :: IO ()
+main = print $ incomplete (Just ())
=====================================
testsuite/tests/pmcheck/should_compile/T17729.stderr
=====================================
@@ -0,0 +1,4 @@
+
+T17729.hs:5:17: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative: Patterns not matched: ((Just _), ())
=====================================
testsuite/tests/pmcheck/should_compile/T18273.hs
=====================================
@@ -0,0 +1,41 @@
+{-# OPTIONS_GHC -fforce-recomp -Wincomplete-patterns #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module Bug where
+
+import Data.Kind
+import Data.Void
+
+type SFalse = SBool 'False
+type STrue = SBool 'True
+
+data SBool :: Bool -> Type where
+ SFalse :: SFalse
+ STrue :: STrue
+
+type family F (b :: Bool) :: Type where
+ F 'False = Void
+ F 'True = ()
+
+data T (b :: Bool)
+ = MkT1
+ | MkT2 !(F b)
+
+ex :: SBool b -> T b -> ()
+ex sb t =
+ case t of
+ MkT1 -> ()
+ MkT2 f ->
+ case sb of
+ STrue -> f
+
+ex2 :: SBool b -> T b -> ()
+ex2 sb t =
+ case t of
+ MkT2 f ->
+ case sb of
+ STrue -> f
+ MkT1 -> ()
=====================================
testsuite/tests/pmcheck/should_compile/T18341.hs
=====================================
@@ -0,0 +1,24 @@
+{-# OPTIONS_GHC -Wincomplete-patterns -fforce-recomp #-}
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE MagicHash #-}
+
+module Lib where
+
+import GHC.Exts
+
+data T = MkT !Int {-# UNPACK #-} !Int Int#
+
+f :: T -> ()
+f (MkT _ _ _) | False = () -- inaccessible
+f (MkT !_ _ _) | False = () -- redundant, not only inaccessible!
+f _ = ()
+
+g :: T -> ()
+g (MkT _ _ _) | False = () -- inaccessible
+g (MkT _ !_ _) | False = () -- redundant, not only inaccessible!
+g _ = ()
+
+h :: T -> ()
+h (MkT _ _ _) | False = () -- inaccessible
+h (MkT _ _ !_) | False = () -- redundant, not only inaccessible!
+h _ = ()
=====================================
testsuite/tests/pmcheck/should_compile/T18341.stderr
=====================================
@@ -0,0 +1,24 @@
+
+T18341.hs:12:18: warning: [-Woverlapping-patterns (in -Wdefault)]
+ Pattern match has inaccessible right hand side
+ In an equation for ‘f’: f (MkT _ _ _) | False = ...
+
+T18341.hs:13:18: warning: [-Woverlapping-patterns (in -Wdefault)]
+ Pattern match is redundant
+ In an equation for ‘f’: f (MkT !_ _ _) | False = ...
+
+T18341.hs:17:18: warning: [-Woverlapping-patterns (in -Wdefault)]
+ Pattern match has inaccessible right hand side
+ In an equation for ‘g’: g (MkT _ _ _) | False = ...
+
+T18341.hs:18:18: warning: [-Woverlapping-patterns (in -Wdefault)]
+ Pattern match is redundant
+ In an equation for ‘g’: g (MkT _ !_ _) | False = ...
+
+T18341.hs:22:18: warning: [-Woverlapping-patterns (in -Wdefault)]
+ Pattern match has inaccessible right hand side
+ In an equation for ‘h’: h (MkT _ _ _) | False = ...
+
+T18341.hs:23:18: warning: [-Woverlapping-patterns (in -Wdefault)]
+ Pattern match is redundant
+ In an equation for ‘h’: h (MkT _ _ !_) | False = ...
=====================================
testsuite/tests/pmcheck/should_compile/all.T
=====================================
@@ -36,6 +36,8 @@ test('T9951b', [], compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T9951', [], compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T10183', [], compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T11303', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns +RTS -M1G -RTS'])
test('T11276', collect_compiler_stats('bytes allocated',10), compile,
@@ -106,12 +108,18 @@ test('T17357', expect_broken(17357), compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T17376', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T17378', normal, compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T17465', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T17646', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T17703', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T17725', normal, compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T17729', normal, compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T17783', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T17977', collect_compiler_stats('bytes allocated',10), compile,
@@ -120,6 +128,10 @@ test('T17977b', collect_compiler_stats('bytes allocated',10), compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T18049', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T18273', normal, compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T18341', normal, compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
# Other tests
test('pmc001', [], compile,
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/d1888d46e4cbb27f7d0a3ba89bf4f69bfc5776f0...6f30cf6b606dbf0e5eeee8106ae3155e5d494670
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/d1888d46e4cbb27f7d0a3ba89bf4f69bfc5776f0...6f30cf6b606dbf0e5eeee8106ae3155e5d494670
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20200703/a81b8809/attachment-0001.html>
More information about the ghc-commits
mailing list