But actually I had hoped we can come up with something more general and less ad-hoc than the behavior of 8.8. Maybe there isn't and 8.8 already lived in the sweet spot.

I think that it's quite fine (maybe desirable even) for error and warning messages to be ad hoc. On Wed, Nov 10, 2021 at 8:29 AM Sebastian Graf <sgraf1337@gmail.com> wrote:

I agree in principle, but then what about data types with strict fields? E.g.

data SMaybe a = SNothing | SJust !a

f :: SMaybe Bool -> () f SNothing = ()

Today, we'd suggest `SJust _`. But the checker can't differentiate between evaluation done by a pattern-match of the user vs. something like a strict field that was unlifted to begin with. So we'd suggest `SJust True` and `SJust False`.

Similarly, we'd case split unlifted data types by default, but not lifted data types.

I think I can easily make the whole function (`GHC.HsToCore.Pmc.Solver.generateInhabitingPatterns`) dependent on whether it's called from an EmptyCase or not, to recover the behavior pre-8.10. But actually I had hoped we can come up with something more general and less ad-hoc than the behavior of 8.8. Maybe there isn't and 8.8 already lived in the sweet spot.

------ Originalnachricht ------ Von: "Richard Eisenberg" <lists@richarde.dev> An: "Sebastian Graf" <sgraf1337@gmail.com> Cc: "ghc-devs" <ghc-devs@haskell.org> Gesendet: 10.11.2021 04:44:50 Betreff: Re: Case split uncovered patterns in warnings or not?

Maybe the answer should depend on whether the scrutinee has already been forced. The new output ("We now say", below) offers up patterns that will change the strictness behavior of the code. The old output did not.

Reading the link below, I see that, previously, there was an inconsistency with -XEmptyCase, which *did* unroll one level of constructor. But maybe that made sense because -XEmptyCase is strict (unlike normal case).

I'm just saying this because I think listing the constructors in the -XEmptyCase case is a good practice, but otherwise I think they're clutterful... and strictness is a perhaps more principled way of making this distinction.

Richard

On Nov 9, 2021, at 8:17 AM, Sebastian Graf <sgraf1337@gmail.com> wrote:

Hi Devs,

In https://gitlab.haskell.org/ghc/ghc/-/issues/20642 we saw that GHC >= 8.10 outputs pattern match warnings a little differently than it used to. Example from there:

{-# OPTIONS_GHC -Wincomplete-uni-patterns #-}foo :: [a] -> [a]foo [] = []foo xs = ys where (_, ys@(_:_)) = splitAt 0 xsmain :: IO ()main = putStrLn $ foo $ "Hello, coverage checker!"

Instead of saying

ListPair.hs:7:3: warning: [-Wincomplete-uni-patterns] Pattern match(es) are non-exhaustive In a pattern binding: Patterns not matched: (_, [])

We now say

ListPair.hs:7:3: warning: [-Wincomplete-uni-patterns] Pattern match(es) are non-exhaustive In a pattern binding: Patterns of type ‘([a], [a])’ not matched: ([], []) ((_:_), [])

E.g., newer versions do (one) case split on pattern variables that haven't even been scrutinised by the pattern match. That amounts to quantitatively more pattern suggestions and for each variable a list of constructors that could be matched on. The motivation for the change is outlined in https://gitlab.haskell.org/ghc/ghc/-/issues/20642#note_390110, but I could easily be swayed not to do the case split. Which arguably is less surprising, as Andreas Abel points out.

Considering the other examples from my post, which would you prefer?

Cheers, Sebastian _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Integer is an interesting example. I think it reveals another issue: exhaustiveness checking should account for abstract data types. If the constructors are not exported, do not case split. - Vlad

On 10 Nov 2021, at 12:48, Oleg Grenrus <oleg.grenrus@iki.fi> wrote:

It should not. Not even when forced.

I have seen an `Integer` constructors presented to me, for example:

module Ex where

foo :: Bool -> Integer -> Integer foo True i = i

With GHC-8.8 the warning is good:

% ghci-8.8.4 -Wall Ex.hs GHCi, version 8.8.4: https://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/phadej/.ghci [1 of 1] Compiling Ex ( Ex.hs, interpreted )

Ex.hs:4:1: warning: [-Wincomplete-patterns] Pattern match(es) are non-exhaustive In an equation for ‘foo’: Patterns not matched: False _ | 4 | foo True i = i | ^^^^^^^^^^^^^^

With GHC-8.10 is straight up awful. I'm glad I don't have to explain it to any beginner, or person who don't know how Integer is implemented. (9.2 is about as bad too).

% ghci-8.10.4 -Wall Ex.hs GHCi, version 8.10.4: https://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/phadej/.ghci [1 of 1] Compiling Ex ( Ex.hs, interpreted )

Ex.hs:4:1: warning: [-Wincomplete-patterns] Pattern match(es) are non-exhaustive In an equation for ‘foo’: Patterns not matched: False (integer-gmp-1.0.3.0:GHC.Integer.Type.S# _) False (integer-gmp-1.0.3.0:GHC.Integer.Type.Jp# _) False (integer-gmp-1.0.3.0:GHC.Integer.Type.Jn# _) | 4 | foo True i = i | ^^^

- Oleg

On 9.11.2021 15.17, Sebastian Graf wrote:

...

Hi Devs,

In https://gitlab.haskell.org/ghc/ghc/-/issues/20642 we saw that GHC >= 8.10 outputs pattern match warnings a little differently than it used to. Example from there:

{-# OPTIONS_GHC -Wincomplete-uni-patterns #-}

foo :: [a] -> [a] foo [] = [] foo xs = ys where (_, ys@(_:_)) = splitAt 0 xs

main :: IO () main = putStrLn $ foo $ "Hello, coverage checker!" Instead of saying

ListPair.hs:7:3: warning: [-Wincomplete-uni-patterns] Pattern match(es) are non-exhaustive In a pattern binding: Patterns not matched: (_, [])

We now say

ListPair.hs:7:3: warning: [-Wincomplete-uni-patterns] Pattern match(es) are non-exhaustive In a pattern binding: Patterns of type ‘([a], [a])’ not matched: ([], []) ((_:_), [])

E.g., newer versions do (one) case split on pattern variables that haven't even been scrutinised by the pattern match. That amounts to quantitatively more pattern suggestions and for each variable a list of constructors that could be matched on. The motivation for the change is outlined in https://gitlab.haskell.org/ghc/ghc/-/issues/20642#note_390110, but I could easily be swayed not to do the case split. Which arguably is less surprising, as Andreas Abel points out.

Considering the other examples from my post, which would you prefer?

Cheers, Sebastian

_______________________________________________ ghc-devs mailing list

ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

---

ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

This is good idea. I think it would work, if you don't consider empty types. There is no way to not export & import uninhabitness of a type. For Void it doesn't matter, but for     newtype Fin j = UnsafeFin { indexFin :: Int }         absurdFin :: Fin Z -> a     absurdFin x = x `seq` error "absurd: Fin Z" as an efficient version of     data Fin n where         FZ :: Fin (S n)         FS :: Fin n -> Fin (S n)     absurdFin :: Fin z -> a     absurdFin x = case x of {} it does. For GADT version users can directly use EmptyCase instead of `absurdFin`, for unsafe&efficient one the `absurdFin` is the only way today. Alternatively (to not exporting safe `Fin Z` uninhabitness), we should be able to say     {-# COMPLETE :: Fin Z #-} i.e. `Fin Z` doesn't need to be matched for pattern match to be complete. - Oleg P.S. I'm not sure if this is relevant to the tickets sgraf linked in his reply. On 10.11.2021 11.51, Vladislav Zavialov wrote:

Integer is an interesting example. I think it reveals another issue: exhaustiveness checking should account for abstract data types. If the constructors are not exported, do not case split.

- Vlad

...

On 10 Nov 2021, at 12:48, Oleg Grenrus <oleg.grenrus@iki.fi> wrote:

It should not. Not even when forced.

I have seen an `Integer` constructors presented to me, for example:

module Ex where

foo :: Bool -> Integer -> Integer foo True i = i

With GHC-8.8 the warning is good:

% ghci-8.8.4 -Wall Ex.hs GHCi, version 8.8.4: https://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/phadej/.ghci [1 of 1] Compiling Ex ( Ex.hs, interpreted )

Ex.hs:4:1: warning: [-Wincomplete-patterns] Pattern match(es) are non-exhaustive In an equation for ‘foo’: Patterns not matched: False _ | 4 | foo True i = i | ^^^^^^^^^^^^^^

With GHC-8.10 is straight up awful. I'm glad I don't have to explain it to any beginner, or person who don't know how Integer is implemented. (9.2 is about as bad too).

% ghci-8.10.4 -Wall Ex.hs GHCi, version 8.10.4: https://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/phadej/.ghci [1 of 1] Compiling Ex ( Ex.hs, interpreted )

Ex.hs:4:1: warning: [-Wincomplete-patterns] Pattern match(es) are non-exhaustive In an equation for ‘foo’: Patterns not matched: False (integer-gmp-1.0.3.0:GHC.Integer.Type.S# _) False (integer-gmp-1.0.3.0:GHC.Integer.Type.Jp# _) False (integer-gmp-1.0.3.0:GHC.Integer.Type.Jn# _) | 4 | foo True i = i | ^^^

- Oleg

On 9.11.2021 15.17, Sebastian Graf wrote:

...

Hi Devs,

In https://gitlab.haskell.org/ghc/ghc/-/issues/20642 we saw that GHC >= 8.10 outputs pattern match warnings a little differently than it used to. Example from there:

{-# OPTIONS_GHC -Wincomplete-uni-patterns #-}

foo :: [a] -> [a] foo [] = [] foo xs = ys where (_, ys@(_:_)) = splitAt 0 xs

main :: IO () main = putStrLn $ foo $ "Hello, coverage checker!" Instead of saying

ListPair.hs:7:3: warning: [-Wincomplete-uni-patterns] Pattern match(es) are non-exhaustive In a pattern binding: Patterns not matched: (_, [])

We now say

ListPair.hs:7:3: warning: [-Wincomplete-uni-patterns] Pattern match(es) are non-exhaustive In a pattern binding: Patterns of type ‘([a], [a])’ not matched: ([], []) ((_:_), [])

E.g., newer versions do (one) case split on pattern variables that haven't even been scrutinised by the pattern match. That amounts to quantitatively more pattern suggestions and for each variable a list of constructors that could be matched on. The motivation for the change is outlined in https://gitlab.haskell.org/ghc/ghc/-/issues/20642#note_390110, but I could easily be swayed not to do the case split. Which arguably is less surprising, as Andreas Abel points out.

Considering the other examples from my post, which would you prefer?

Cheers, Sebastian

_______________________________________________ ghc-devs mailing list

ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

---

ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs