Re: Case split uncovered patterns in warnings or not?

[Oleg Grenrus]

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 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  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
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re[2]: Case split uncovered patterns in warnings or not?

[Sebastian Graf]

Yes, but that is an entirely different issue: See 
https://gitlab.haskell.org/ghc/ghc/-/issues/13964, 
https://gitlab.haskell.org/ghc/ghc/-/issues/20311 and my problems in 
https://gitlab.haskell.org/ghc/ghc/-/merge_requests/4116#note_301577 and 
following. Help is appreciated there, I don't know how to get the 
necessary information in `DsM`. Would need to poke at `mi_exports`, 
which is quite unreachable at that point. I'd probably have to add a 
field to the `DsGblEnv`.


I agree that Integer is another nail in the coffin, but only by 
coincidence. As I said in the issue, if you do an EmptyCase on `Integer` 
(which you rarely should do), then you'd be presented with the abstract 
constructors in GHC 8.8, too.


As for the issue at hand, I'll go for "case split on EmptyCase only", 
which should get back the behavior from 8.8.


-- Originalnachricht --
Von: "Vladislav Zavialov" 
An: "Oleg Grenrus" 
Cc: "ghc-devs" 
Gesendet: 10.11.2021 10:51:03
Betreff: Re: Case split uncovered patterns in warnings or not?


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  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


___
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

Re: Case split uncovered patterns in warnings or not?

[Vladislav Zavialov]

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  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

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

Re: Case split uncovered patterns in warnings or not?

[Oleg Grenrus]

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

Re: Re[2]: Case split uncovered patterns in warnings or not?

[Spiwack, Arnaud]

> 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  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" 
> An: "Sebastian Graf" 
> Cc: "ghc-devs" 
> 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  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-exhaustiveIn a pattern binding: Patterns not matched: (_, [])
>
> We now say
>
> ListPair.hs:7:3: warning: [-Wincomplete-uni-patterns]Pattern match(es) 
> are non-exhaustiveIn 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
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs