Constraint solver regression in 9.2

Summary

When porting some generics-sop code from GHC 8.10 to GHC 9.2, I discovered a regression in the type checker.

Steps to reproduce

Run GHC on the following program:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module ConstraintTest2 where

import Data.Kind

type family Code a :: [[Type]]

type IsWrappedType a x = Code a ~ '[ '[ x ] ]
type IsProductType a xs = Code a ~ '[ xs ]

type family Head (xs :: [a]) :: a where
  Head (x : xs) = x

type ProductCode a = Head (Code a)
type WrappedCode a = Head (Head (Code a))

wrappedTypeTo :: IsWrappedType a x => x -> a
wrappedTypeTo = undefined

to :: SOP (Code a) -> a
to = undefined

data SOP (xss :: [[a]])

type WrappedProduct a = (IsWrappedType a (WrappedCode a), IsProductType (WrappedCode a) (ProductCode (WrappedCode a)))

process :: (SOP '[ xs ] -> a) -> a
process = undefined

-- works with 8.10 and 9.0, fails with 9.2
test :: WrappedProduct a => a
test = process (wrappedTypeTo . to)

Expected behavior

I expect the program to compile, as it does with GHC 8.10 and GHC 9.0. However, with GHC 9.2, I get:

/home/andres/trans/ConstraintTest2.hs:37:17: error:
    • Could not deduce: Code a ~ '[ '[b0]]
        arising from a use of ‘wrappedTypeTo’
      from the context: WrappedProduct a
        bound by the type signature for:
                   test :: forall a. WrappedProduct a => a
        at /home/andres/trans/ConstraintTest2.hs:36:1-29
      The type variable ‘b0’ is ambiguous
    • In the first argument of ‘(.)’, namely ‘wrappedTypeTo’
      In the first argument of ‘process’, namely ‘(wrappedTypeTo . to)’
      In the expression: process (wrappedTypeTo . to)
    • Relevant bindings include
        test :: a (bound at /home/andres/trans/ConstraintTest2.hs:37:1)
   |
37 | test = process (wrappedTypeTo . to)
   |                 ^^^^^^^^^^^^^

/home/andres/trans/ConstraintTest2.hs:37:33: error:
    • Could not deduce: Code b0 ~ '[xs0]
      from the context: WrappedProduct a
        bound by the type signature for:
                   test :: forall a. WrappedProduct a => a
        at /home/andres/trans/ConstraintTest2.hs:36:1-29
      Expected: SOP '[xs0] -> b0
        Actual: SOP (Code b0) -> b0
      The type variables ‘b0’, ‘xs0’ are ambiguous
    • In the second argument of ‘(.)’, namely ‘to’
      In the first argument of ‘process’, namely ‘(wrappedTypeTo . to)’
      In the expression: process (wrappedTypeTo . to)
   |
37 | test = process (wrappedTypeTo . to)
   |                                 ^^

Environment

• GHC version used: 9.2.2