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