Pattern match is redundant if present, non-exhaustive if missing
Consider
{-# OPTIONS_GHC -Wall -Wno-missing-signatures -Wno-unused-imports #-}
module Bug where
import Data.Void
data T a = MkT1 Int | MkT2 !a
f (MkT1 x) = x
f (MkT2 y) = absurd y
GHC will warn that the match against MkT2
is redundant. This is because the use of absurd
tells us that a ~ Void
and the strict field in MkT2
can never be inhabited.
But if we comment that line out, then the pattern-match is non-exhaustive, because we've lost the information that a ~ Void
.
Both statements are correct: When present, the equation is redundant. When absent, the equation is needed.
The problem is that it's redundant at runtime, but quite informative at compile-time. GHC doesn't recognize this nuance.
I actually ran into this in !4149 (closed), where the added cleverness in the solver deals better with type families used in GHC's TTG, and this behavior arose in the cvt
helper function in Haddock.Convert
.
I have no solution to offer. GHC really is correct in both cases, but it's awfully confusing -- even for someone who knows how this all works under the hood. But the only solution to improve the user experience here would require some sort of tracking of where critical information in type inference originally arose, and then giving the user a hint when it arises (only) from an otherwise-redundant bit of code. I'm raising this ticket in case someone is cleverer than I at improving the situation. In my concrete case (and, I presume, in all other similar cases), the problem is avoided with an extra type annotation, which I will add and then move on.