[GHC] #11503: TypeError woes (incl. pattern match checker)
#11503: TypeError woes (incl. pattern match checker) -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- When I say {{{ {-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeFamilies, UndecidableInstances #-} {-# OPTIONS_GHC -fwarn-incomplete-patterns #-} module Bug where import GHC.TypeLits import GHC.Exts ( Constraint ) type family NotInt a where NotInt Int = TypeError (Text "That's Int, silly.") NotInt _ = (() :: Constraint) data T a where MkT1 :: a -> T a MkT2 :: NotInt a => T a foo :: T Int -> Int foo (MkT1 x) = x }}} I get {{{ Bug.hs:19:1: warning: Pattern match(es) are non-exhaustive In an equation for ‘foo’: Patterns not matched: MkT2 }}} But I shouldn't. Even worse, perhaps, GHC accepts my pattern-match against `MkT2` if I add it. If I change the `TypeError` to `False ~ True`, I get the correct behavior. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11503 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11503: TypeError woes (incl. pattern match checker) -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | 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: => PatternMatchWarnings Comment: I think you are saying that {{{ type family NotInt a where NotInt Int = False ~ True NotInt _ = (() :: Constraint) }}} makes everything work. That's because the pattern-match warning infrastructure treats `False ~ True` as definitely insoluble. But apparently it doesn't treat `TypeErorr blah` as definitely insoluble. That's because when we solve `[G] NotInt Int`, we get `[G] TypeError ... ~ fsk, [G] fsk`, and neither is treated as insoluble. I'm sure this can be dealt with, but it'll need a little care. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11503#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11503: TypeError woes (incl. pattern match checker) -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | PatternMatchWarnings, | CustomTypeErrors Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14141 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: PatternMatchWarnings => PatternMatchWarnings, CustomTypeErrors * related: => #14141 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11503#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11503: TypeError woes (incl. pattern match checker) -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | PatternMatchWarnings, | CustomTypeErrors Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14141 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): I ran into this issue a few days ago, and it really is annoying. We're forced to choose between a constraint the pattern checker will work with properly (`'True ~ 'False`) and a constraint that will give a good error message when accidentally matching against `MkT2` (`TypeError ...`). There's a sort of workaround, but it's really horrible: instead of `'True ~ 'False`, use something like `"" ~ "This is an error message!"`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11503#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11503: TypeError woes (incl. pattern match checker) -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: | PatternMatchWarnings, | CustomTypeErrors Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: #14141 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by dfeuer): * cc: dfeuer (added) * failure: None/Unknown => Incorrect error/warning at compile-time * milestone: => 8.6.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11503#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11503: TypeError woes (incl. pattern match checker) -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: | PatternMatchWarnings, | CustomTypeErrors Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: #14141 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): Simon, I imagine there's a broad reason somewhere for {{{ [G] c ~ fsk, [G] fsk }}} not to be simplified to {{{ [G] c }}} Assuming that's the case I suspect maybe we should track known insoluble constraints the way we track known-bottoming expressions. Since `TypeError ... ~ fsk` and `TypeError ...` is insoluble, we could conclude that `fsk` is insoluble. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11503#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11503: TypeError woes (incl. pattern match checker) -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.10.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: | PatternMatchWarnings, | CustomTypeErrors Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: #14141, #16377 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: #14141 => #14141, #16377 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11503#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC