Constraint solver: Reject Givens that are unsatisfiable by a pre-image analysis of a closed type family
Summary
This issue tracks an idea to improve pattern-match coverage checking from #22652. I'm pretty sure that the constraint solver is the right location to implement this fix, as the reproducer below by @RyanGlScott from #22652 (comment 480491) does not actually need to run the coverage checker to reproduce.
Steps to reproduce
Consider
{-# LANGUAGE DataKinds, TypeFamilies, GADTs #-}
{-# OPTIONS_GHC -Winaccessible-code -Werror #-}
module Bug where
data T = Z | S
data ST n where
SS :: ST S
type family F n where
F Z = Z
F S = Z
f :: F m ~ n => ST m -> ST n -> ()
f _ SS = ()
Currently, GHC does not warn at all when compiling this code:
$ ghc98 Bug.hs -fforce-recomp -Winaccessible-code
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Expected behavior
I would expect this code to emit a -Winaccessible-code
warning for f
, because
- The match on
SS
implies thatn ~ S
- But
F m ~ S
is not satisfiable for anym
I would imagine that the constraint solver could employ a very simple kind of pre-image analysis on the definition of F
to figure out what kinds of values it cannot return; similar to OtherCon
unfoldings in Core. (To support recursive definitions, one could employ a very simple fixpoint iteration.) If constructor C
cannot be returned by a type family Fam
, then Fam a b c ~ C
is rejected.