[Haskell-cafe] Spurious [-Woverlapping-patterns] -- [cont] ghc should be able to deduce correct use of partial functions
Olaf Klinke
olf at aatal-apotheke.de
Sat Apr 27 19:03:13 UTC 2024
> I think this is a similar 'failure to deduce' partiality as last
> week's
> thread; but the other way round (and with ViewPatterns) -- at GHC
> 8.10.7:
>
> GHCi> :set -XViewPatterns
> GHCi> :set -Wincomplete-patterns -- also warns overlapping
> GHCi> (\x -> case x of {((\(Just j) -> j) -> j2) -> j2; Nothing ->
> 'N'})
> Nothing
>
> ===> <interactive>: warning: [-Woverlapping-patterns]
> Pattern match is redundant
> In a case alternative: Nothing -> ...
> *** Exception: <interactive>:16:21-34: Non-exhaustive patterns in
> lambda
>
> (Same Warning then same Exception if I compile the code.)
I think what we see here is an instance of the fact that all checks
must break down in presence of view patterns. If I parsed your code
correctly, the case analysis has two branches. The first uses a view
pattern with a function, call it v for the moment. The result of v is
bound to another pattern, in your case the wildcard j2 and that is
returned as-is, so in pseudo-Haskell:
case (v x) of j2 -> j2
case x of Nothing -> 'N'
Now your view function v happens to be partial, it pattern-matches its
argument and only provides a branch for the Just case.
v = \(Just j) -> j = Data.Maybe.fromJust
That is why you see the exception when you call this function with
'Nothing'. And indeed the second match is redundant insofar as the view
pattern will evaluate v for any x. Since v could be anything, like
unsafePerformIO (lauchMissiles >> return j)
GHC does not examine this and thus can not decide that v does not match
the cases that the Nothing branch does. If you swap the two branches
and make the view pattern the last one, then both the exception and the
warning go away.
Olaf
More information about the Haskell-Cafe
mailing list