[GHC] #12949: Pattern coverage mistake
#12949: Pattern coverage mistake -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: Incorrect Unknown/Multiple | error/warning at compile-time Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- I disabled syntax highlighting below; the bugs highlighting single quotes made the code unreadable. {{{ {-# LANGUAGE DataKinds, TypeFamilies, GADTs, TypeOperators, ScopedTypeVariables, ConstraintKinds, StandaloneDeriving #-} {-# OPTIONS_GHC -Wall #-} import Data.Constraint import Data.Type.Bool -- Bool singletons data Boolly b where Falsey :: Boolly 'False Truey :: Boolly 'True deriving instance Show (Boolly b) class KnownBool b where knownBool :: Boolly b instance KnownBool 'False where knownBool = Falsey instance KnownBool 'True where knownBool = Truey -- OrRel a b r expresses all the usual implications inherent -- in the statement that r ~ (a || b). type OrRel (a :: Bool) (b :: Bool) (r :: Bool) :: Constraint = (r ~ (a || b), If r (If (Not a) (b ~ 'True) (() :: Constraint), If (Not b) (a ~ 'True) (() :: Constraint)) (a ~ 'False, b ~ 'False)) -- Given known Bools, their disjunction is also known abr :: forall a b r p1 p2 . (OrRel a b r, KnownBool a, KnownBool b) => p1 a -> p2 b -> Dict (KnownBool r) abr _ _ = case knownBool :: Boolly a of Truey -> Dict Falsey -> case knownBool :: Boolly b of Truey -> Dict -- Problematic match Falsey -> Dict }}} The trouble is that GHC warns that the problematic match is redundant, which it is not. If I remove it, GHC ''fails'' to warn that the patterns are incomplete, which they are. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12949 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12949: Pattern coverage mistake -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): Note that everything works as expected if I pass in the `Boolly` values explicitly. Perhaps the pattern coverage checker is confusing `knownBool` called at different types? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12949#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12949: Pattern coverage mistake -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): This does indeed look like a bug to me. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12949#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12949: Pattern coverage mistake -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by mpickering): * cc: gkaracha (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12949#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12949: Pattern coverage mistake -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by gkaracha): * keywords: => PatternMatchWarnings Comment: Ah, yes, I think so too. First #11984 freshened variables too much (I still haven't managed to fix it), now this freshens them too little. I will take a look at this one too. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12949#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12949: Pattern coverage mistake -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: gkaracha Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * owner: => gkaracha * milestone: => 8.2.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12949#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12949: Pattern coverage mistake -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: gkaracha Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by gkaracha): Replying to [comment:1 dfeuer]:
Note that everything works as expected if I pass in the `Boolly` values explicitly. Perhaps the pattern coverage checker is confusing `knownBool` called at different types?
Indeed you are right, this is not a bug in the type constraints that the checker generates but the term constraints. I expected the `knownBool`s to be already desugared to `(knownBool $dKnownBool_a)` and `(knownBool $dKnownBool_b)` since they are overloaded but I was mistaken. Hence, it now (wrongly) generates `{knownBool ~ Falsey, knownBool ~ Truey}` which is of course unsatisfiable. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12949#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12949: Pattern coverage mistake -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: gkaracha Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by gkaracha): I guess I could fix this by - Turning `Name` back into `Id` in the checker (incl. the term oracle) - Checking equality on term variables taking their type into account, something like this: {{{#!hs tmEqVar :: Id -> Id -> Bool tmEqVar x1 x2 = (idName x1 == idName x2) && (idType x1 `eqType` idType x2) }}} Does that make sense? PS. I am not happy to have types in the term oracle (it's not as modular as I liked it to be) but I don't know of any other way to "restore" the implicit invariant that each variable has only **one type**. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12949#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12949: Pattern coverage mistake -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: gkaracha Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): I believe the instance selection is all done in the type checker. Hopefully someone can tell you how to get that info! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12949#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12949: Pattern coverage mistake -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: gkaracha Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
Indeed you are right, this is not a bug in the type constraints that the checker generates but the term constraints. I expected the knownBools to be already desugared to (knownBool $dKnownBool_a) and (knownBool $dKnownBool_b) since they are overloaded but I was mistaken.
I'm going to need more guidance before I can help. Can you give instructions to reproduce the bit you think is unexpected? I compiled the program (adding a definition for `Dict` which you omitted), with `-ddump-ds` and got {{{ ... ds_d3Xn = knownBool @ a $dKnownBool_a3Ux } in ... ds_d3Xo = knownBool @ b $dKnownBool_a3UL } in }}} which is what you expect. This is post-desugaring. Before desugaring there'll be a `HsWrapper` involved. Anyway, please show me specifically what you think it unexpected. ---------------- Incidentally, the constraint signatures don't seem to work. Compiling {{{ type T a = Eq a :: Constraint }}} yields a syntax error, as does {{{ type T a :: Constraint = Eq a }}} I must be doing something stupid. But what? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12949#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
Indeed you are right, this is not a bug in the type constraints that
#12949: Pattern coverage mistake -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: gkaracha Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by gkaracha): Replying to [comment:9 simonpj]: the checker generates but the term constraints. I expected the knownBools to be already desugared to (knownBool $dKnownBool_a) and (knownBool $dKnownBool_b) since they are overloaded but I was mistaken.
I'm going to need more guidance before I can help. Can you give
instructions to reproduce the bit you think is unexpected?
I compiled the program (adding a definition for `Dict` which you
{{{ ... ds_d3Xn = knownBool @ a $dKnownBool_a3Ux } in ... ds_d3Xo = knownBool @ b $dKnownBool_a3UL } in
}}} which is what you expect. This is post-desugaring. Before desugaring
omitted), with `-ddump-ds` and got there'll be a `HsWrapper` involved. Ah, great, thanks! This may be sufficient: I think that `translatePat` in `deSugar/Check.hs` just needs to look at the wrapper in the `CoPat` case then. It already inspects it for dropping trivial coercions, as an optimization. I'll look into it and ping you if anything else gets in the way (I hope not). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12949#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12949: Pattern coverage mistake -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: gkaracha Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): In case it's helpful, I've come up with a much simpler case: {{{#!hs {-# LANGUAGE ScopedTypeVariables #-} module Exh where class Foo a where foo :: Maybe a data Result a b = Neither | This a | That b | Both a b q :: forall a b . (Foo a, Foo b) => Result a b q = case foo :: Maybe a of Nothing -> case foo :: Maybe b of Nothing -> Neither Just c -> That c Just i -> case foo :: Maybe b of Nothing -> This i Just c -> Both i c }}} This produces the following warnings, both of them incorrect: {{{ Exh.hs:13:20: warning: [-Woverlapping-patterns] Pattern match is redundant In a case alternative: Just c -> ... | 13 | Just c -> That c | ^^^^^^^^^^^^^^^^ Exh.hs:15:20: warning: [-Woverlapping-patterns] Pattern match is redundant In a case alternative: Nothing -> ... | 15 | Nothing -> This i | ^^^^^^^^^^^^^^^^^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12949#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12949: Pattern coverage checker ignores dictionary arguments -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: gkaracha Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12949#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12949: Pattern coverage checker ignores dictionary arguments -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: gkaracha Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): gkaracha, does that help? Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12949#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12949: Pattern coverage checker ignores dictionary arguments -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: gkaracha Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by sighingnow): Hello, I'm working on this ticket and now I can tell what's going wrong with the case in comment:11. I think I need some help to go further and submit the patch. Look at the example in comment:11: {{{#!hs q :: forall a b . (Foo a, Foo b) => Result a b q = case foo :: Maybe a of Nothing -> case foo :: Maybe b of Nothing -> Neither Just c -> That c }}} When do `checkMatches` on inner `case` statement, we first call `mkInitialUncovered` to set up a NameEnv, in this function we use `getTmCsDs` to obtain the initial name env, we have {{{#!hs [(ds_d14i, foo), (ds_d14h, Nothing), (ds_d14h, foo)] }}} Nothing that these two `foo` have different `Id` (type), but the same `Name`. We then translate them as `ComplexEq`, only keeping the `Name` in `PmExprVar`. Then we get the `initTmState`. In `ConVar` case of `pmcheckHd`, we have ComplexEq `(ds_d14i, Just $pm_d14m)` and use `solveOneEq` to decide whether it is a valid candidate `PmCon`. In `solveOneEq`, we first do deep substitution by looking up the `Name` of `PmExprVar` from env. Now `ds_d14i` is replaced with `foo` and further replaced with `Nothing`, then `solveOneEq` fails and the `Just` pattern is redundant. --------------------------------------------- To solve this, we need to consider both name and type of variables when do substitution. In comment:7 gkaracha proposed that
Turning Name back into Id in the checker
Should we move from `PmExprVar Name` to `PmExprVar Id` ? In `varDeepLookup`, when find the `PmExpr` from PrVarEnv, we could first check it's type then do further substitution. Do that make sense ? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12949#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC