Pattern match checker stumbles over reasonably tricky pattern-match
In !2192 (comment 247043) Simon finally convinced me that it's reasonable to record type constraints arising from a constructor application in a CoreExpr
in the pattern-match checkers type oracle. Namely
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ViewPatterns #-}
module Lib where
data S a where
S1 :: S Int
S2 :: S Bool
data T where
K :: S a -> a -> T
f1 :: S Int -> ()
f1 s = case K @Int s 3 of K S1 _ -> ()
f2 :: S Int -> ()
f2 s = case K @Int s 3 of K s' _ -> case s' of S1 -> ()
data T2 where
K2 :: (a -> S a) -> a -> T2
g1 :: (Int -> S Int) -> ()
g1 h = case K2 @Int h 3 of K2 h' (h' -> S1) -> ()
g2 :: (Int -> S Int) -> ()
g2 h = case K2 @Int h 3 of K2 h' i' -> case h' i' of S1 -> ()
All pattern matches are exhaustive, yet we currently only flag f1
as such. It's easy to also flag the other cases if we simply record that the a
bound by K
(and K2
, respectively) is subject to the constraint a ~ Int
, which is easiest to see by looking at the case
's scrutinee.
Taking f2
as the example, the not-so-easy way would be to see that s' ~ s
(we already make that connection!), and then from the fact that s :: S Int
derive that S2
is not a possible constructor for s
, so it can't be for s'
. Sadly, apparently we don't make the connection to s
's type.