Opened 5 weeks ago
Last modified 4 weeks ago
#14253 new bug
Pattern match checker mistakenly concludes pattern match on pattern synonym is unreachable
Reported by: | bgamari | Owned by: | |
---|---|---|---|
Priority: | high | Milestone: | 8.4.1 |
Component: | Compiler | Version: | 8.2.1 |
Keywords: | PatternSynonyms, PatternMatchWarnings | Cc: | George, gkaracha, dfeuer, RyanGlScott |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | GHC rejects valid program | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | #11984, #14098 | Differential Rev(s): | Phab:D4005 |
Wiki Page: |
Description
Consider this program,
{-# LANGUAGE GADTs #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeInType #-} module Test where import GHC.Exts import Data.Kind data TypeRep (a :: k) where Con :: TypeRep (a :: k) TrFun :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) (a :: TYPE r1) (b :: TYPE r2). TypeRep a -> TypeRep b -> TypeRep (a -> b) pattern Fun :: forall k (fun :: k). () => forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) (arg :: TYPE r1) (res :: TYPE r2). (k ~ Type, fun ~~ (arg -> res)) => TypeRep arg -> TypeRep res -> TypeRep fun pattern Fun arg res <- TrFun arg res where Fun arg res = undefined data Dynamic where Dynamic :: forall a. TypeRep a -> a -> Dynamic -- Removing this allows compilation to proceed {-# COMPLETE Con #-} dynApply :: Dynamic -> Dynamic -> Maybe Dynamic -- Changing Fun to TrFun allows compilation to proceed dynApply (Dynamic (Fun ta tr) f) (Dynamic ta' x) = undefined dynApply _ _ = Nothing
As written the program fails with,
test.hs:34:1: warning: [-Woverlapping-patterns] Pattern match has inaccessible right hand side In an equation for ‘dynApply’: dynApply (Dynamic (Fun ta tr) f) (Dynamic ta' x) = ... | 34 | dynApply (Dynamic (Fun ta tr) f) (Dynamic ta' x) = undefined | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
This can be worked around by doing one of the following,
- Removing the
COMPLETE
pragma - Changing the use of the
Fun
pattern synonym into a use of theTrFun
constructor.
Something is quite wrong here.
Change History (14)
comment:1 Changed 5 weeks ago by
Cc: | gkaracha dfeuer added |
---|
comment:2 Changed 5 weeks ago by
Cc: | RyanGlScott added |
---|---|
Keywords: | PatternSynonyms PatternMatchWarnings added |
comment:3 follow-up: 4 Changed 5 weeks ago by
I'm puzzled though. The {-# COMPLETE MkT1 #-}
pragma seems like a manifest lie. It claims that any matching on MkT2
is inaccessible doesn't it?
comment:4 Changed 5 weeks ago by
Replying to simonpj:
I'm puzzled though. The
{-# COMPLETE MkT1 #-}
pragma seems like a manifest lie. It claims that any matching onMkT2
is inaccessible doesn't it?
COMPLETE
pragmas are allowed to be lies. Perhaps values built from MkT1
are never visible outside this module.
comment:5 Changed 5 weeks ago by
OK, but then lies might give rise to error messages or warnings that lie, mightn't they. As here.
We need a specification of the expected behaviour of lying COMPLETE pragmas before we can discuss what programs like these "should" do. Or we could say "if the pragma lies, the compiler can do what it likes".
comment:6 Changed 5 weeks ago by
Ah, I think Ryan's simplification goes a bit too far, perhaps. I think you'll find Ben's original version convincing.
comment:7 follow-up: 8 Changed 5 weeks ago by
I'm not sure why the original program would be any more honest, since it claims that matching on TrFun
is inaccessible, right? That is, Con
is to MkT1
as TrFun
is to MkT2
as Fun
is to MkT2'
as Dynamic
is to S
as dynApply
is to u
. Or am I missing something?
comment:8 Changed 5 weeks ago by
Replying to RyanGlScott:
I'm not sure why the original program would be any more honest, since it claims that matching on
TrFun
is inaccessible, right? That is,Con
is toMkT1
asTrFun
is toMkT2
asFun
is toMkT2'
asDynamic
is toS
asdynApply
is tou
. Or am I missing something?
Ah, simply because I didn't read it correctly. Ben came to this dishonest reduction from a perfectly honest example!
comment:9 Changed 5 weeks ago by
Regardless of the example's moral integrity, I posit that it exhibits buggy behavior.
First, let's try to hammer out what should happen here. There's something of a specification buried in the annals of the GHC wiki here. (Why is this not in the users' guide?) The relevant bit is:
When the pattern match checker requests a set of constructors for a type constructor
T
, we now return a list of sets which include the normal data constructor set and also anyCOMPLETE
pragmas of typeT
. We then try each of these sets, not warning if any of them are a perfect match. In the case the match isn't perfect, we select one of the branches of the search depending on how good the result is.The results are prioritised in this order.
- Fewest uncovered clauses
- Fewest redundant clauses
- Fewest inaccessible clauses
- Whether the match comes from a
COMPLETE
pragma or the built-in set of data constructors for a type constructor.
In the example above, we're matching on something of type T
, so we have the built-in constructor set {MkT1, MkT2}
as well as the COMPLETE
set {MkT1}
. Since u
only matches on MkT2'
, the latter set {MkT1}
(the COMPLETE
set) has the fewest number of uncovered clauses, so we use that for reporting warnings. Therefore, the error that we would expect to get (but don't, due to this bug) is:
Pattern match(es) are non-exhaustive In a case alternative: Patterns not matched: MkS MkT1
Does that sound agreeable?
comment:10 Changed 5 weeks ago by
comment:11 Changed 5 weeks ago by
Related Tickets: | → #11984, #14098 |
---|
Phab:D4005 adds the rules to the GHC users' guide (proofreaders wanted).
As for why this bug happens in the first place, I have a strong hunch that there's a symptom in common with #11984 (and #14098). The reason is because while this give a warning:
u :: S -> Bool u (MkS MkT2') = True
Pattern match has inaccessible right hand side In an equation for ‘u’: u (MkS MkT2') = ...
You can work around the issue using the same trick in https://ghc.haskell.org/trac/ghc/ticket/11984#comment:7 :
u :: S -> Bool u (MkS x) = case x of MkT2' -> True
After this, instead of emitting the garbage inaccessible right-hand-side warning from before, GHC will warn:
Pattern match(es) are non-exhaustive In a case alternative: Patterns not matched: MkT1
As we would expect. So now we need to figure out why there is a discrepancy between the pattern match checker's coverage of case
and nested constructors. (I'm hoping I gain some insight after talking to SPJ about this part of the codebase tomorrow.)
comment:14 Changed 4 weeks ago by
Differential Rev(s): | → Phab:D4005 |
---|
Here is a much simpler way to trigger the issue:
The fact that
MkT2'
occurs inside of another constructorMkS
seems to be important, since changingu
to be of typeT -> Bool
and matching directly onMkT2'
in the first case resolves the issue.