[GHC] #11390: GHC does not warn about redundant equations
#11390: GHC does not warn about redundant equations -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Keywords: warnings | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Given the Phab:D1535 effort in GHC 8.0 I was curious how an example from Richard's post [https://typesandkinds.wordpress.com/2015/09/09/what-are- type-families/ What are type families?] would fare: {{{ % ghci -Wall -XTypeFamilies -ignore-dot-ghci GHCi, version 8.1.20160105: http://www.haskell.org/ghc/ :? for help Prelude> :set +m Prelude> type family F1 a where Prelude| F1 Int = Bool Prelude| Prelude> let Prelude| sillyId :: F1 Char -> F1 Char Prelude| sillyId x = x Prelude| Prelude> }}} This seems to fly, even though as the blog post noted, ”[...] sillyId can’t ever be called on a value.” Isn't the clause redundant and should be defined using `EmptyCase` (#2431) as `sillyId x = case x of {}`? It seems GHC doesn't care that the pattern match in the equation `absurd2 _ = ...` is redundant either: {{{#!hs data Void absurd1 :: Void -> a; absurd1 = \case absurd2 :: Void -> a absurd2 _ = undefined }}} Is this intended or known behaviour? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11390 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11390: GHC does not warn about redundant patterns -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: warnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11390#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11390: GHC does not warn about redundant patterns -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: warnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by Iceland_jack: Old description:
Given the Phab:D1535 effort in GHC 8.0 I was curious how an example from Richard's post [https://typesandkinds.wordpress.com/2015/09/09/what-are- type-families/ What are type families?] would fare:
{{{ % ghci -Wall -XTypeFamilies -ignore-dot-ghci GHCi, version 8.1.20160105: http://www.haskell.org/ghc/ :? for help Prelude> :set +m Prelude> type family F1 a where Prelude| F1 Int = Bool Prelude| Prelude> let Prelude| sillyId :: F1 Char -> F1 Char Prelude| sillyId x = x Prelude| Prelude> }}}
This seems to fly, even though as the blog post noted, ”[...] sillyId can’t ever be called on a value.” Isn't the clause redundant and should be defined using `EmptyCase` (#2431) as `sillyId x = case x of {}`?
It seems GHC doesn't care that the pattern match in the equation `absurd2 _ = ...` is redundant either: {{{#!hs data Void
absurd1 :: Void -> a; absurd1 = \case
absurd2 :: Void -> a absurd2 _ = undefined }}}
Is this intended or known behaviour?
New description: Given the Phab:D1535 effort in GHC 8.0 I was curious how an example from Richard's post [https://typesandkinds.wordpress.com/2015/09/09/what-are- type-families/ What are type families?] would fare: {{{ % ghci -Wall -XTypeFamilies -ignore-dot-ghci GHCi, version 8.1.20160105: http://www.haskell.org/ghc/ :? for help Prelude> :set +m Prelude> type family F1 a where Prelude| F1 Int = Bool Prelude| Prelude> let Prelude| sillyId :: F1 Char -> F1 Char Prelude| sillyId x = x Prelude| Prelude> }}} This seems to fly, even though as the blog post noted, ”[...] sillyId can’t ever be called on a value.” Isn't the clause redundant and should be defined using `EmptyCase` (#2431) as `sillyId x = case x of {}`? It seems GHC doesn't care that the pattern match in the equation `absurd2 _ = ...` is redundant either: {{{#!hs data Void absurd1 :: Void -> a absurd1 = \case absurd2 :: Void -> a absurd2 _ = undefined }}} Is this intended or known behaviour? -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11390#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11390: GHC does not warn about redundant patterns -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: warnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): Empty data declarations are Haskell 2010, so it doesn't seem reasonable to give a warning that suggests something outside the Haskell 2010 language. If EmptyCase is already on, though, it could make sense to issue a warning in your second example. I don't understand your first example. Isn't the clause `sillyId x = case x of {}` just as "redundant" as the clause `sillyId x = x` was in the first place? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11390#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11390: GHC does not warn about redundant patterns -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: warnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): I thought `case x of {}` indicated to the compiler that the clause is empty ([http://downloads.haskell.org/~ghc/master/users- guide/glasgow_exts.html#empty-case-alternatives Empty case alternative]) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11390#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11390: GHC does not warn about redundant patterns -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: warnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): I would say that `case x of {}` is just a case expression with no alternatives. It is, itself, still an ordinary expression. So both versions look like `sillyId x = <expr>` and should be equivalent as far as redundancy of the ''outer'' pattern match, the one done by `sillyId`, is concerned. Since you cannot write a definition with 0 equations, this "redundancy" is unavoidable. (Unless you use LambdaCase and EmptyCase, I guess.) Are you suggesting treating `case x of {}` as some kind of special form? Also, I'm not sure a "stuck" type family application is really empty in the same sense as an empty data type. But #10746 makes it hard to tell what GHC thinks about this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11390#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
With dependently-typed features it is more useful (see Trac #2431). For example, consider these two candidate definitions of absurd:
{{{#!hs data a :==: b where Refl :: a :==: a
absurd :: True :~: False -> a absurd x = error "absurd" -- (A) absurd x = case x of {} -- (B) }}}
We much prefer (B). Why? Because GHC can figure out that `(True :~: False)` is an empty type. So (B) has no partiality and GHC should be able to compile with [http://downloads.haskell.org/~ghc/master/users-guide /using-warnings.html#ghc-flag--Wincomplete-patterns -Wincomplete-
#11390: GHC does not warn about redundant patterns -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: warnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): I thought that was what the documentation for `EmptyCase` is alluding to: patterns]. (Though the pattern match checking is not yet clever enough to do that.) On the other hand (A) looks dangerous, and GHC doesn’t check to make sure that, in fact, the function can never get called. I wasn't sure whether the "Though the pattern match checking is not yet clever enough to do that." statement had changed in 8, I'll edit the code to enable `LambdaCase` as well. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11390#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11390: GHC does not warn about redundant patterns -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: warnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by Iceland_jack: Old description:
Given the Phab:D1535 effort in GHC 8.0 I was curious how an example from Richard's post [https://typesandkinds.wordpress.com/2015/09/09/what-are- type-families/ What are type families?] would fare:
{{{ % ghci -Wall -XTypeFamilies -ignore-dot-ghci GHCi, version 8.1.20160105: http://www.haskell.org/ghc/ :? for help Prelude> :set +m Prelude> type family F1 a where Prelude| F1 Int = Bool Prelude| Prelude> let Prelude| sillyId :: F1 Char -> F1 Char Prelude| sillyId x = x Prelude| Prelude> }}}
This seems to fly, even though as the blog post noted, ”[...] sillyId can’t ever be called on a value.” Isn't the clause redundant and should be defined using `EmptyCase` (#2431) as `sillyId x = case x of {}`?
It seems GHC doesn't care that the pattern match in the equation `absurd2 _ = ...` is redundant either: {{{#!hs data Void
absurd1 :: Void -> a absurd1 = \case
absurd2 :: Void -> a absurd2 _ = undefined }}}
Is this intended or known behaviour?
New description: Given the Phab:D1535 effort in GHC 8.0 I was curious how an example from Richard's post [https://typesandkinds.wordpress.com/2015/09/09/what-are- type-families/ What are type families?] would fare: {{{ % ghci -Wall -XTypeFamilies -ignore-dot-ghci GHCi, version 8.1.20160105: http://www.haskell.org/ghc/ :? for help Prelude> :set +m Prelude> type family F1 a where Prelude| F1 Int = Bool Prelude| Prelude> let Prelude| sillyId :: F1 Char -> F1 Char Prelude| sillyId x = x Prelude| Prelude> }}} This seems to fly, even though as the blog post noted, ”[...] sillyId can’t ever be called on a value.” Isn't the clause redundant and should be defined using `EmptyCase` (#2431) as `sillyId = \case`? It seems GHC doesn't care that the pattern match in the equation `absurd2 _ = ...` is redundant either: {{{#!hs data Void absurd1 :: Void -> a absurd1 = \case absurd2 :: Void -> a absurd2 _ = undefined }}} Is this intended or known behaviour? -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11390#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11390: GHC does not warn about redundant patterns -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: warnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Old description:
Given the Phab:D1535 effort in GHC 8.0 I was curious how an example from Richard's post [https://typesandkinds.wordpress.com/2015/09/09/what-are- type-families/ What are type families?] would fare:
{{{ % ghci -Wall -XTypeFamilies -ignore-dot-ghci GHCi, version 8.1.20160105: http://www.haskell.org/ghc/ :? for help Prelude> :set +m Prelude> type family F1 a where Prelude| F1 Int = Bool Prelude| Prelude> let Prelude| sillyId :: F1 Char -> F1 Char Prelude| sillyId x = x Prelude| Prelude> }}}
This seems to fly, even though as the blog post noted, ”[...] sillyId can’t ever be called on a value.” Isn't the clause redundant and should be defined using `EmptyCase` (#2431) as `sillyId = \case`?
It seems GHC doesn't care that the pattern match in the equation `absurd2 _ = ...` is redundant either: {{{#!hs data Void
absurd1 :: Void -> a absurd1 = \case
absurd2 :: Void -> a absurd2 _ = undefined }}}
Is this intended or known behaviour?
New description: Given the Phab:D1535 effort in GHC 8.0 I was curious how an example from Richard's post [https://typesandkinds.wordpress.com/2015/09/09/what-are- type-families/ What are type families?] would fare: {{{ % ghci -Wall -XTypeFamilies -ignore-dot-ghci GHCi, version 8.1.20160105: http://www.haskell.org/ghc/ :? for help Prelude> :set +m Prelude> type family F1 a where Prelude| F1 Int = Bool Prelude| Prelude> let Prelude| sillyId :: F1 Char -> F1 Char Prelude| sillyId x = x Prelude| Prelude> }}} This seems to fly, even though as the blog post noted, ”[...] sillyId can’t ever be called on a value.” Isn't the clause redundant and should be defined using `EmptyCase` (#2431) as `sillyId = \case`? It seems GHC doesn't care that the pattern match in the equation `absurd2 _ = ...` is redundant either: {{{#!hs data Void absurd1 :: Void -> a absurd1 = \case absurd2 :: Void -> a absurd2 _ = undefined }}} Is this intended or known behaviour? -- Comment (by rwbarton): The manual there is talking about partiality, or completeness of pattern matches, not redundancy. (B) is complete because the pattern match in `absurd` is complete, and the pattern match in the `case` is also complete. But the pattern match in `absurd` is "redundant", regardless of what happens on the right-hand side of the equation. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11390#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11390: GHC does not warn about redundant patterns -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: warnings, | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: warnings => warnings, PatternMatchWarnings -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11390#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11390: GHC does not warn about redundant patterns -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: warnings, | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by gkaracha): Actually nothing is redundant in the above examples. As we discuss in the paper (section about laziness), `(sillyId undefined)` will give you the right hand-side so the clause: {{{#!hs sillyId x = x }}} is not redundant at all. Of course, this is not the case for: {{{#!hs sillyId2 :: F1 Char -> F1 Char sillyId2 (!x) = x }}} because it is strict in the argument, so no WHNF can have the type `F1 Char`. But even in this case, the clause is not actually redundant, it just has an inaccessible RHS (remember this is not Agda). Pattern matching is not just used for discrimination in Haskell but also for evaluation, which I see as a side effect. Hence, the clause may have an inaccessible RHS, but by removing it the expression is not evaluated and you change the semantics of `sillyId2`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11390#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11390: GHC does not warn about redundant patterns -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: warnings, | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): Good point. If the return type was a type with values, the clause would ''really'' not be redundant! {{{ sillyFun :: F1 Char -> String sillyFun x = "hi" }}} Surely it doesn't make sense for redundancy of a pattern match to depend on what sort of thing is on the right hand side? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11390#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11390: GHC does not warn about redundant patterns -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: warnings, | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I agree with George (gkaracha). `sillyId x = x` can't be called on a value, but Haskell isn't call-by-value. I will use `Void` instead of `F1 Char`, because the type family bit isn't the interesting part here. {{{ silly1 :: Void -> Void silly1 x = x silly2 :: Void -> Void silly2 x = error "urk" }}} `silly1 undefined` and `silly2 undefined` have different runtime behavior; the pattern is not redundant. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11390#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11390: GHC does not warn about redundant patterns -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: warnings, | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): In that case, GHC's behavior is correct and we can close this ticket, right? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11390#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11390: GHC does not warn about redundant patterns -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: warnings, | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by gkaracha): Yes, I think we can close this :-) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11390#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11390: GHC does not warn about redundant patterns -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: invalid | Keywords: warnings, | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by gkaracha): * status: new => closed * resolution: => invalid -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11390#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC