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