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 (closed). 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 that n ~ S
• But F m ~ S is not satisfiable for any m

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.