Commit 1593debf authored by Sebastian Graf's avatar Sebastian Graf Committed by Marge Bot

Check EmptyCase by simply adding a non-void constraint

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
parent 487ede42
Pipeline #12230 failed with stages
in 533 minutes and 59 seconds
This diff is collapsed.
This diff is collapsed.
......@@ -128,44 +128,6 @@ instance Eq PmLit where
pmLitType :: PmLit -> Type
pmLitType (PmLit ty _) = ty
-- | Type of a 'PmAltCon'
pmAltConType :: PmAltCon -> [Type] -> Type
pmAltConType (PmAltLit lit) _arg_tys = ASSERT( null _arg_tys ) pmLitType lit
pmAltConType (PmAltConLike con) arg_tys = conLikeResTy con arg_tys
instance Outputable PmLitValue where
ppr (PmLitInt i) = ppr i
ppr (PmLitRat r) = ppr (double (fromRat r)) -- good enough
ppr (PmLitChar c) = pprHsChar c
ppr (PmLitString s) = pprHsString s
ppr (PmLitOverInt n i) = minuses n (ppr i)
ppr (PmLitOverRat n r) = minuses n (ppr (double (fromRat r)))
ppr (PmLitOverString s) = pprHsString s
-- Take care of negated literals
minuses :: Int -> SDoc -> SDoc
minuses n sdoc = iterate (\sdoc -> parens (char '-' <> sdoc)) sdoc !! n
instance Outputable PmLit where
ppr (PmLit ty v) = ppr v <> suffix
where
-- Some ad-hoc hackery for displaying proper lit suffixes based on type
tbl = [ (intPrimTy, primIntSuffix)
, (int64PrimTy, primInt64Suffix)
, (wordPrimTy, primWordSuffix)
, (word64PrimTy, primWord64Suffix)
, (charPrimTy, primCharSuffix)
, (floatPrimTy, primFloatSuffix)
, (doublePrimTy, primDoubleSuffix) ]
suffix = fromMaybe empty (snd <$> find (eqType ty . fst) tbl)
instance Outputable PmAltCon where
ppr (PmAltConLike cl) = ppr cl
ppr (PmAltLit l) = ppr l
instance Outputable PmEquality where
ppr = text . show
-- | Undecidable equality for values represented by 'ConLike's.
-- See Note [Undecidable Equality for PmAltCons].
-- 'PatSynCon's aren't enforced to be generative, so two syntactically different
......@@ -222,6 +184,11 @@ eqPmAltCon _ _ = PossiblyOverlap
instance Eq PmAltCon where
a == b = eqPmAltCon a b == Equal
-- | Type of a 'PmAltCon'
pmAltConType :: PmAltCon -> [Type] -> Type
pmAltConType (PmAltLit lit) _arg_tys = ASSERT( null _arg_tys ) pmLitType lit
pmAltConType (PmAltConLike con) arg_tys = conLikeResTy con arg_tys
{- Note [Undecidable Equality for PmAltCons]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Equality on overloaded literals is undecidable in the general case. Consider
......@@ -364,20 +331,53 @@ coreExprAsPmLit e = case collectArgs e of
| otherwise
= False
instance Outputable PmLitValue where
ppr (PmLitInt i) = ppr i
ppr (PmLitRat r) = ppr (double (fromRat r)) -- good enough
ppr (PmLitChar c) = pprHsChar c
ppr (PmLitString s) = pprHsString s
ppr (PmLitOverInt n i) = minuses n (ppr i)
ppr (PmLitOverRat n r) = minuses n (ppr (double (fromRat r)))
ppr (PmLitOverString s) = pprHsString s
-- Take care of negated literals
minuses :: Int -> SDoc -> SDoc
minuses n sdoc = iterate (\sdoc -> parens (char '-' <> sdoc)) sdoc !! n
instance Outputable PmLit where
ppr (PmLit ty v) = ppr v <> suffix
where
-- Some ad-hoc hackery for displaying proper lit suffixes based on type
tbl = [ (intPrimTy, primIntSuffix)
, (int64PrimTy, primInt64Suffix)
, (wordPrimTy, primWordSuffix)
, (word64PrimTy, primWord64Suffix)
, (charPrimTy, primCharSuffix)
, (floatPrimTy, primFloatSuffix)
, (doublePrimTy, primDoubleSuffix) ]
suffix = fromMaybe empty (snd <$> find (eqType ty . fst) tbl)
instance Outputable PmAltCon where
ppr (PmAltConLike cl) = ppr cl
ppr (PmAltLit l) = ppr l
instance Outputable PmEquality where
ppr = text . show
type ConLikeSet = UniqDSet ConLike
-- | A data type caching the results of 'completeMatchConLikes' with support for
-- deletion of contructors that were already matched on.
-- deletion of constructors that were already matched on.
data PossibleMatches
= PM TyCon (NonEmpty.NonEmpty ConLikeSet)
-- ^ Each ConLikeSet is a (subset of) the constructors in a COMPLETE pragma
= PM (NonEmpty.NonEmpty ConLikeSet)
-- ^ Each ConLikeSet is a (subset of) the constructors in a COMPLETE set
-- 'NonEmpty' because the empty case would mean that the type has no COMPLETE
-- set at all, for which we have 'NoPM'
-- set at all, for which we have 'NoPM'.
| NoPM
-- ^ No COMPLETE set for this type (yet). Think of overloaded literals.
instance Outputable PossibleMatches where
ppr (PM _tc cs) = ppr (NonEmpty.toList cs)
ppr (PM cs) = ppr (NonEmpty.toList cs)
ppr NoPM = text "<NoPM>"
-- | Either @Indirect x@, meaning the value is represented by that of @x@, or
......
......@@ -241,7 +241,11 @@ tcCompleteSigs sigs =
mkMatch :: [ConLike] -> TyCon -> CompleteMatch
mkMatch cls ty_con = CompleteMatch {
completeMatchConLikes = map conLikeName cls,
-- foldM is a left-fold and will have accumulated the ConLikes in
-- the reverse order. foldrM would accumulate in the correct order,
-- but would type-check the last ConLike first, which might also be
-- confusing from the user's perspective. Hence reverse here.
completeMatchConLikes = reverse (map conLikeName cls),
completeMatchTyCon = tyConName ty_con
}
doOne _ = return Nothing
......@@ -287,7 +291,10 @@ tcCompleteSigs sigs =
<+> parens (quotes (ppr tc)
<+> text "resp."
<+> quotes (ppr tc'))
in mapMaybeM (addLocM doOne) sigs
-- For some reason I haven't investigated further, the signatures come in
-- backwards wrt. declaration order. So we reverse them here, because it makes
-- a difference for incomplete match suggestions.
in mapMaybeM (addLocM doOne) (reverse sigs) -- process in declaration order
tcHsBootSigs :: [(RecFlag, LHsBinds GhcRn)] -> [LSig GhcRn] -> TcM [Id]
-- A hs-boot file has only one BindGroup, and it only has type
......
......@@ -693,7 +693,7 @@ It does *not* reduce type or data family applications or look through newtypes.
Why is this useful? As one example, when coverage-checking an EmptyCase
expression, it's possible that the type of the scrutinee will only reduce
if some local equalities are solved for. See "Wrinkle: Local equalities"
in Note [Type normalisation for EmptyCase] in Check.
in Note [Type normalisation] in Check.
To accomplish its stated goal, tcNormalise first feeds the local constraints
into solveSimpleGivens, then stuffs the argument type in a CHoleCan, and feeds
......
......@@ -3,4 +3,7 @@ KindEqualities.hs:25:1: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In an equation for ‘zero’:
Patterns not matched:
TyApp (TyApp p _) _ where p is not one of {TyInt}
TyApp (TyApp _ _) TyInt
TyApp (TyApp _ _) TyBool
TyApp (TyApp _ _) TyMaybe
TyApp (TyApp _ _) (TyApp _ _)
{-# OPTIONS_GHC -Wincomplete-patterns -fforce-recomp #-}
{-# LANGUAGE PatternSynonyms #-}
module Lib where
data B = T | F
pattern P :: B
pattern P = T
{-# COMPLETE P, F #-}
f :: B -> ()
f P = ()
pattern Q :: B
pattern Q = T
{-# COMPLETE T, Q #-}
g :: B -> ()
g Q = ()
T17386.hs:11:1: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In an equation for ‘f’: Patterns not matched: F
T17386.hs:18:1: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In an equation for ‘g’: Patterns not matched: T
......@@ -16,7 +16,7 @@ test('completesig15', normal, compile_fail, [''])
test('T13021', normal, compile, [''])
test('T13363a', normal, compile, [''])
test('T13363b', normal, compile, [''])
test('T13717', expect_broken('13717'), compile, [''])
test('T13717', normal, compile, [''])
test('T13964', normal, compile, [''])
test('T13965', normal, compile, [''])
test('T14059a', normal, compile, [''])
......@@ -24,3 +24,4 @@ test('T14059b', expect_broken('14059'), compile, [''])
test('T14253', normal, compile, [''])
test('T14851', normal, compile, [''])
test('T17149', normal, compile, [''])
test('T17386', normal, compile, [''])
......@@ -25,5 +25,5 @@ completesig06.hs:29:1: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In an equation for ‘m5’:
Patterns not matched:
A _
B _
A D
B D
......@@ -9,4 +9,4 @@ EmptyCase003.hs:32:6: warning: [-Wincomplete-patterns (in -Wextra)]
EmptyCase003.hs:37:6: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In a case alternative: Patterns not matched: _ :: Char
In a case alternative: Patterns not matched: _ :: C Int
......@@ -30,4 +30,4 @@ EmptyCase005.hs:91:8: warning: [-Wincomplete-patterns (in -Wextra)]
EmptyCase005.hs:101:8: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In a case alternative: Patterns not matched: _ :: H Char
In a case alternative: Patterns not matched: _ :: H Int
EmptyCase007.hs:21:7: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In a case alternative: Patterns not matched: _ :: Foo2 a
In a case alternative: Patterns not matched: Foo2 _
EmptyCase007.hs:25:7: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In a case alternative: Patterns not matched: _ :: Foo2 (a, a)
In a case alternative: Patterns not matched: Foo2 _
EmptyCase007.hs:33:7: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
......@@ -17,7 +17,7 @@ EmptyCase007.hs:37:7: warning: [-Wincomplete-patterns (in -Wextra)]
EmptyCase007.hs:44:17: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In a case alternative: Patterns not matched: _ :: Char
In a case alternative: Patterns not matched: _ :: FA Char
EmptyCase007.hs:48:7: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
......
......@@ -8,7 +8,7 @@ EmptyCase008.hs:17:7: warning: [-Wincomplete-patterns (in -Wextra)]
EmptyCase008.hs:21:7: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In a case alternative: Patterns not matched: _ :: Foo3 a
In a case alternative: Patterns not matched: Foo3 _
EmptyCase008.hs:40:7: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
......@@ -16,4 +16,4 @@ EmptyCase008.hs:40:7: warning: [-Wincomplete-patterns (in -Wextra)]
EmptyCase008.hs:48:7: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In a case alternative: Patterns not matched: _ :: Foo4 a b
In a case alternative: Patterns not matched: Foo4 _
EmptyCase009.hs:21:9: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In a case alternative: Patterns not matched: _ :: Bar f
In a case alternative: Patterns not matched: Bar _
EmptyCase009.hs:33:7: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
......
......@@ -31,7 +31,7 @@ EmptyCase010.hs:45:7: warning: [-Wincomplete-patterns (in -Wextra)]
EmptyCase010.hs:57:7: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In a case alternative: Patterns not matched: _ :: Baz (DC ()) a
In a case alternative: Patterns not matched: Baz _
EmptyCase010.hs:69:7: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
......@@ -39,4 +39,4 @@ EmptyCase010.hs:69:7: warning: [-Wincomplete-patterns (in -Wextra)]
EmptyCase010.hs:73:9: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In a case alternative: Patterns not matched: _ :: Baz f a
In a case alternative: Patterns not matched: Baz _
T10746.hs:9:10: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In a case alternative:
......
T11336b.hs:25:1: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In an equation for ‘fun’: Patterns not matched: _ :: Proxy a
In an equation for ‘fun’: Patterns not matched: Proxy
......@@ -10,8 +10,16 @@ T11822.hs:33:1: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In an equation for ‘mkTreeNode’:
Patterns not matched:
_ (Data.Sequence.Internal.Seq _) _ p where p is not one of {0}
_ (Data.Sequence.Internal.Seq _) _ p where p is not one of {0}
_ (Data.Sequence.Internal.Seq _) _ _
_ (Data.Sequence.Internal.Seq _) _ _
_ (Data.Sequence.Internal.Seq Data.Sequence.Internal.EmptyT)
(Data.Set.Internal.Bin _ _ _ _) p
where p is not one of {0}
_ (Data.Sequence.Internal.Seq Data.Sequence.Internal.EmptyT)
Data.Set.Internal.Tip p
where p is not one of {0}
_ (Data.Sequence.Internal.Seq (Data.Sequence.Internal.Single _))
(Data.Set.Internal.Bin _ _ _ _) p
where p is not one of {0}
_ (Data.Sequence.Internal.Seq (Data.Sequence.Internal.Single _))
Data.Set.Internal.Tip p
where p is not one of {0}
...
{-# LANGUAGE BangPatterns #-}
module Lib where
data T1 a = T1 a
......@@ -10,6 +11,7 @@ f _ _ = ()
g :: T2 a -> Bool -> ()
g _ True = ()
g (T2 _) True = ()
g (T2 _) True = () -- redundant
g !_ True = () -- inaccessible
g _ _ = ()
T17248.hs:8:1: warning: [-Woverlapping-patterns (in -Wdefault)]
T17248.hs:9:1: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match has inaccessible right hand side
In an equation for ‘f’: f (T1 _) True = ...
T17248.hs:14:1: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match is redundant
In an equation for ‘g’: g (T2 _) True = ...
T17248.hs:15:1: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match has inaccessible right hand side
In an equation for ‘g’: g !_ True = ...
{-# OPTIONS_GHC -Wincomplete-patterns -fforce-recomp #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE BangPatterns #-}
module Lib where
import Data.Void
strictConst :: a -> b -> a
strictConst a b = seq b a
pattern F <- (const False -> True)
pattern SF <- (strictConst False -> True)
-- | The second clause is redundant, really, because (the matcher of) 'F' is
-- not strict in its argument. As a result, the third clause is *not*
-- redundant, but inaccessible RHS! Deleting the third clause would be unsound.
-- This is bad, especially because this outcome depends entirely on the
-- strictness of 'F's matcher.
f :: Bool -> Bool -> ()
f _ True = ()
f F True = ()
f !_ True = ()
f _ _ = ()
-- | In this example, the second clause really is inaccessible RHS (because SF
-- is a strict match). And as a result, the third clause *is* redundant.
f2 :: Bool -> Bool -> ()
f2 _ True = ()
f2 SF True = ()
f2 !_ True = ()
f2 _ _ = ()
pattern T <- (const True -> True)
{-# COMPLETE T, F :: Void #-}
-- | But we consider COMPLETE signatures to cover bottom. Hence the last clause
-- here should be redunant, not inaccessible RHS.
f3 :: Void -> ()
f3 T = ()
f3 F = ()
f3 !_ = ()
-- The following is related to the same issue:
-- | The following function definition is exhaustive.
-- Its clauses are *not* inaccessible RHS, because neither
-- pattern synonym is strict.
g :: Void -> ()
g F = ()
g T = ()
T17357.hs:22:1: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match has inaccessible right hand side
In an equation for ‘f’: f F True = ...
T17357.hs:23:1: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match has inaccessible right hand side
In an equation for ‘f’: f !_ True = ...
T17357.hs:30:1: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match has inaccessible right hand side
In an equation for ‘f2’: f2 SF True = ...
T17357.hs:31:1: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match has inaccessible right hand side
In an equation for ‘f2’: f2 !_ True = ...
T17357.hs:42:1: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match is redundant
In an equation for ‘f3’: f3 !_ = ...
module Lib where
import Data.Void
f :: Void -> ()
f x = case x of _ -> ()
......@@ -4,9 +4,9 @@ T2204.hs:6:1: warning: [-Wincomplete-patterns (in -Wextra)]
In an equation for ‘f’:
Patterns not matched:
('0':'1':_:_)
('0':p:_) where p is not one of {'1'}
['0', p] where p is not one of {'1'}
('0':p:_:_) where p is not one of {'1'}
['0']
(p:_) where p is not one of {'0'}
...
T2204.hs:9:1: warning: [-Wincomplete-patterns (in -Wextra)]
......
......@@ -4,7 +4,7 @@ T9951b.hs:7:1: warning: [-Wincomplete-patterns (in -Wextra)]
In an equation for ‘f’:
Patterns not matched:
('a':'b':_:_)
('a':p:_) where p is not one of {'b'}
['a', p] where p is not one of {'b'}
('a':p:_:_) where p is not one of {'b'}
['a']
(p:_) where p is not one of {'a'}
...
......@@ -8,7 +8,12 @@ TooManyDeltas.hs:14:1: warning:
TooManyDeltas.hs:14:1: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In an equation for ‘f’: Patterns not matched: _ _
In an equation for ‘f’:
Patterns not matched:
A A
A B
B A
B B
TooManyDeltas.hs:19:1: warning:
Pattern match checker ran into -fmax-pmcheck-models=0 limit, so
......
......@@ -100,7 +100,11 @@ test('T17219', expect_broken(17219), compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T17234', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T17248', expect_broken(17248), compile,
test('T17248', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T17357', expect_broken(17357), compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T17376', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
# Other tests
......
......@@ -10,8 +10,8 @@ pmc007.hs:12:1: warning: [-Wincomplete-patterns (in -Wextra)]
Patterns not matched:
('a':'b':_:_)
('a':'c':_:_)
('a':p:_) where p is not one of {'b', 'c'}
['a']
['a', p] where p is not one of {'b', 'c'}
('a':p:_:_) where p is not one of {'b', 'c'}
...
pmc007.hs:18:11: warning: [-Wincomplete-patterns (in -Wextra)]
......@@ -20,6 +20,6 @@ pmc007.hs:18:11: warning: [-Wincomplete-patterns (in -Wextra)]
Patterns not matched:
('a':'b':_:_)
('a':'c':_:_)
('a':p:_) where p is not one of {'b', 'c'}
['a']
['a', p] where p is not one of {'b', 'c'}
('a':p:_:_) where p is not one of {'b', 'c'}
...
pmc009.hs:10:1: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In an equation for ‘addPatSynSelector’:
Patterns not matched: _ :: LHsBind p
In an equation for ‘addPatSynSelector’: Patterns not matched: L _ _
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment