Re: Case split uncovered patterns in warnings or not?

10 Nov 2021

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