Regression in superclass checking of instances

See master ticket #22912 (closed)

Summary

GHC is rejecting some instances of classes involving type families in their superclasses, that it previously accepted.

Steps to reproduce

Minimized example:

{-# LANGUAGE TypeFamilies,
  TypeOperators, DataKinds, ConstraintKinds, UndecidableSuperClasses, UndecidableInstances,
  FlexibleInstances, MultiParamTypeClasses, FlexibleContexts, AllowAmbiguousTypes
 #-}

module R where

import Data.Proxy (Proxy(..))
import Data.Kind (Type)
import Data.Type.Bool

class Functor (If y Maybe Maybe) => C (y :: Bool) where
  p :: Proxy y

instance (S yf yg, y ~ (yf || yg)) => C y where
  p = Proxy

class Functor (If (yf || yg) Maybe Maybe) => S yf yg where
  pS :: Proxy '(yf, yg)

Expected (and actual on GHC 9.0 and prior): Should compile.

Actual (GHC 9.2.1): Error message below.

R.hs:15:10: error:
    • Could not deduce (Functor (If y Maybe Maybe))
        arising from the superclasses of an instance declaration
      from the context: (S yf yg, y ~ (yf || yg))
        bound by the instance declaration at local/r.hs:15:10-41
    • In the instance declaration for ‘C y’
   |
15 | instance (S yf yg, y ~ (yf || yg)) => C y where
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Environment

• GHC version used: 9.2.1

---

EDIT (by @rae):

Despite this being labeled a regression, it turns out that older GHCs were wrong in accepting programs like this in the first place. See #20666 (comment 393745) for a runtime loop possible in GHC 8.10.7.