GHC panic with a code with type equality constraints with doubly applied type family

Summary

With the following code which should not pass type checking, GHC panic at PostTc phase when doing lookupIdSubst. The code has type equality of form F1 (F2 x) ~ F3 y, and I think that's where the bug is triggered, but the panic happens only when combined with other statements in do-notation. (otherwise, usual type error happened, so this is my best minimization up to now).

Steps to reproduce

{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}

module Main where

class C1 b where
  type F1 b

class C2 (m :: * -> *) where
  type F2 m

class C3 r where
  type F3 r

class G t m where
  g :: m a -> t m a

data Y

data X e a

data H a

data S a

fun1 :: X e ()
fun1 = undefined

fun2 :: S ()
fun2 = undefined

fun3 :: H ()
fun3 = undefined

fun4 :: (F3 r ~ F1 (F2 m)) => r -> m ()
fun4 = undefined

test :: (C2 m, F2 m ~ Y) => m ()
test = do
  fun1
  fun2
  g fun3
  fun4 undefined

main :: IO ()
main = pure ()

when running GHC, one will see the following panic error.

$ ghc Panic.hs
[1 of 2] Compiling Main             ( Panic.hs, Panic.o )

Panic.hs:11:16: warning: [GHC-39567] [-Wstar-is-type]
    Using ‘*’ (or its Unicode variant) to mean ‘Data.Kind.Type’
    relies on the StarIsType extension, which will become
    deprecated in the future.
    Suggested fix: Use ‘Type’ from ‘Data.Kind’ instead.
   |
11 | class C2 (m :: * -> *) where
   |                ^

Panic.hs:11:21: warning: [GHC-39567] [-Wstar-is-type]
    Using ‘*’ (or its Unicode variant) to mean ‘Data.Kind.Type’
    relies on the StarIsType extension, which will become
    deprecated in the future.
    Suggested fix: Use ‘Type’ from ‘Data.Kind’ instead.
   |
11 | class C2 (m :: * -> *) where
   |                     ^

Panic.hs:37:15: warning: [GHC-58520] [-Wtype-equality-requires-operators]
    The use of ‘~’ without TypeOperators
    will become an error in a future GHC release.
    Suggested fix: Perhaps you intended to use TypeOperators
   |
37 | fun4 :: (F3 r ~ F1 (F2 m)) => r -> m ()
   |               ^

Panic.hs:40:21: warning: [GHC-58520] [-Wtype-equality-requires-operators]
    The use of ‘~’ without TypeOperators
    will become an error in a future GHC release.
    Suggested fix: Perhaps you intended to use TypeOperators
   |
40 | test :: (C2 m, F2 m ~ Y) => m ()
   |                     ^

<no location info>: error:
    panic! (the 'impossible' happened)
  GHC version 9.6.2:
	lookupIdSubst
  $dMonad_aWA
  InScope {$dIP_aUI $dIP_aUN m_aUW $dC2_aUX $d~_aUY $krep_aWW
           $krep_aWX $krep_aWY $krep_aWZ $krep_aX0 $krep_aX1 $krep_aX2
           $krep_aX3 $krep_aX4 fun1 fun2 fun3 fun4 $tcC1 $tc'C:C1 $tcC2
           $tc'C:C2 $tcC3 $tc'C:C3 $tcG $tcY $tcX $tcH $tcS $trModule}
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/GHC/Utils/Panic.hs:189:37 in ghc:GHC.Utils.Panic
        pprPanic, called at compiler/GHC/Core/Subst.hs:197:17 in ghc:GHC.Core.Subst
  CallStack (from HasCallStack):
    panic, called at compiler/GHC/Utils/Error.hs:454:29 in ghc:GHC.Utils.Error

Expected behavior

This should give a type error and stop there, not proceeding to PostTc phase.

Environment

• GHC version used: ghc 9.6.2

• Operating System: macOS Ventura 13.5.2