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