[GHC] #13717: Pattern synonym exhaustiveness checks don't play well with EmptyCase
#13717: Pattern synonym exhaustiveness checks don't play well with EmptyCase -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler | Version: 8.2.1-rc1 Keywords: | Operating System: Unknown/Multiple PatternSynonyms, | PatternMatchWarnings | Architecture: | Type of failure: Incorrect Unknown/Multiple | error/warning at compile-time Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- In #8779, mpickering added a `COMPLETE` pragma to allow exhaustiveness checking for matches involving pattern synonyms. Unfortunately, there is still one piece missing: the interaction with `EmptyCase`. Suppose I write {{{#!hs newtype Fin (n :: Nat) = Fin Natural -- constructor not exported pattern FZ :: () => forall m. n ~ 'S m => Fin n pattern FS :: () => n ~ 'S m => Fin m -> Fin n {-# COMPLETE FZ, FS #-} }}} I would very much like to be able to write {{{#!hs finZAbsurd :: Fin 'Z -> Void finZAbsurd x = case x of }}} but this gives me a pattern coverage warning! That's certainly not what we want. I believe what we actually want is this: When checking empty case, check that ''at least one'' complete pattern set is impossible. In this case, it would see two complete pattern sets: the built-in `{Fin}` and the user-decreed `{FZ, FS}`. Since neither `FZ` nor `FS` have matching types, we should conclude that the empty case is fine. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13717 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13717: Pattern synonym exhaustiveness checks don't play well with EmptyCase -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler | Version: 8.2.1-rc1 Resolution: | Keywords: | PatternSynonyms, | 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: | -------------------------------------+------------------------------------- Description changed by dfeuer: @@ -8,1 +8,1 @@ - pattern FZ :: () => forall m. n ~ 'S m => Fin n + pattern FZ :: () => n ~ 'S m => Fin n New description: In #8779, mpickering added a `COMPLETE` pragma to allow exhaustiveness checking for matches involving pattern synonyms. Unfortunately, there is still one piece missing: the interaction with `EmptyCase`. Suppose I write {{{#!hs newtype Fin (n :: Nat) = Fin Natural -- constructor not exported pattern FZ :: () => n ~ 'S m => Fin n pattern FS :: () => n ~ 'S m => Fin m -> Fin n {-# COMPLETE FZ, FS #-} }}} I would very much like to be able to write {{{#!hs finZAbsurd :: Fin 'Z -> Void finZAbsurd x = case x of }}} but this gives me a pattern coverage warning! That's certainly not what we want. I believe what we actually want is this: When checking empty case, check that ''at least one'' complete pattern set is impossible. In this case, it would see two complete pattern sets: the built-in `{Fin}` and the user-decreed `{FZ, FS}`. Since neither `FZ` nor `FS` have matching types, we should conclude that the empty case is fine. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13717#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13717: Pattern synonym exhaustiveness checks don't play well with EmptyCase -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler | Version: 8.2.1-rc1 Resolution: | Keywords: | PatternSynonyms, | 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 Iceland_jack): * cc: Iceland_jack (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13717#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13717: Pattern synonym exhaustiveness checks don't play well with EmptyCase -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler | Version: 8.2.1-rc1 Resolution: | Keywords: | PatternSynonyms, | 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 RyanGlScott): I tried to reproduce this error, but I couldn't. I don't know what implementations for `FZ` and `FS` you had in mind, so I tried whipping up my own example from scratch: {{{#!hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PatternSynonyms #-} {-# OPTIONS_GHC -Wall #-} module T (T(TInt, TBool), tCharAbsurd1) where import Data.Void data T a where MkTInt :: T Int MkTBool :: T Bool pattern TInt :: () => n ~ Int => T n pattern TInt = MkTInt pattern TBool :: () => n ~ Bool => T n pattern TBool = MkTBool {-# COMPLETE TInt, TBool #-} tCharAbsurd1 :: T Char -> Void tCharAbsurd1 x = case x of {} }}} This, however, compiles without any warnings. I even tried using `T` in another module: {{{#!hs {-# LANGUAGE EmptyCase #-} {-# OPTIONS_GHC -Wall #-} module Bug where import Data.Void import T tCharAbsurd2 :: T Char -> Void tCharAbsurd2 x = case x of {} }}} This too compiles without warning: {{{ $ ghc/inplace/bin/ghc-stage2 --interactive Bug.hs GHCi, version 8.3.20170516: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 2] Compiling T ( T.hs, interpreted ) [2 of 2] Compiling Bug ( Bug.hs, interpreted ) Ok, modules loaded: Bug, T. }}} How did you get this supposed pattern coverage warning? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13717#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13717: Pattern synonym exhaustiveness checks don't play well with EmptyCase -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler | Version: 8.2.1-rc1 Resolution: | Keywords: | PatternSynonyms, | 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): Here's a full reproduction: {{{#!hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE Trustworthy #-} module Fin (Nat (..), Fin (FZ, FS), FinView (..), viewFin) where import Numeric.Natural import Unsafe.Coerce data Nat = Z | S Nat -- Fin *must* be exported abstractly (or placed in an Unsafe -- module) to maintain type safety. newtype Fin (n :: Nat) = Fin Natural deriving instance Show (Fin n) data FinView n where VZ :: FinView ('S n) VS :: !(Fin n) -> FinView ('S n) viewFin :: Fin n -> FinView n viewFin (Fin 0) = unsafeCoerce VZ viewFin (Fin n) = unsafeCoerce (VS (Fin (n - 1))) pattern FZ :: () => n ~ 'S m => Fin n pattern FZ <- (viewFin -> VZ) where FZ = Fin 0 pattern FS :: () => n ~ 'S m => Fin m -> Fin n pattern FS m <- (viewFin -> VS m) where FS (Fin m) = Fin (1 + m) {-# COMPLETE FZ, FS #-} }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13717#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13717: Pattern synonym exhaustiveness checks don't play well with EmptyCase -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler | Version: 8.2.1-rc1 Resolution: | Keywords: | PatternSynonyms, | 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): For the record, I can implement `finZAbsurd` in a messier way that the pattern checker accepts: {{{#!hs finZAbsurd :: Fin 'Z -> a finZAbsurd = finZAbsurd' Refl where finZAbsurd' :: n :~: 'Z -> Fin n -> a finZAbsurd' pf FZ = case pf of finZAbsurd' pf (FS _) = case pf of }}} but that's a lot uglier. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13717#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13717: Pattern synonym exhaustiveness checks don't play well with EmptyCase -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler | Version: 8.2.1-rc1 Resolution: | Keywords: | PatternSynonyms, | 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 RyanGlScott): dfeuer, thanks. Now I see why my example didn't trigger any warnings: the definition of the `T` type itself (i.e., the fact that it was a GADT) was what ruled out the possibility of matching on any of its constructors in `tCharAbsurd`. On the other hand, `Fin` does not have this property, and you're relying on the types of the conlikes in its `COMPLETE` set to rule out the possibility of matching anything. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13717#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC