Constraint solver regression in 9.2

Summary

While trying to make the generics-sop and sop-core packages compatible with GHC 9.2, I discovered a regression in the constraint solver. The included program compiles at with GHC 9.0.1, GHC 8.8.4, GHC 8.6.5, GHC 8.4.4, GHC 8.2.2, but it fails with GHC 9.2 with the following error message:

AllEq.hs:19:21: error:
    • Couldn't match type ‘ys0’ with ‘Head ys0 : Tail ys0’
        arising from a use of ‘convert’
    • In the second argument of ‘const’, namely ‘(convert xs)’
      In the expression: const () (convert xs)
      In an equation for ‘test’: test xs = const () (convert xs)
   |
19 | test xs = const () (convert xs)
   |                     ^^^^^^^

Steps to reproduce

Run ghc or ghci on the following file:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module AllEq where

import Data.Kind
import Data.Proxy

convert :: (AllEq xs ys) => Proxy xs -> Proxy ys
convert p = Proxy

-- Works with ghc up to 9.0. Fails with ghc 9.2.
test :: Proxy '[Char, Bool] -> ()
test xs = const () (convert xs)

class (AllEqF xs ys, SameShapeAs xs ys) => AllEq (xs :: [a]) (ys :: [a])
instance (AllEqF xs ys, SameShapeAs xs ys) => AllEq xs ys

type family SameShapeAs (xs :: [a]) (ys :: [a]) :: Constraint where
  SameShapeAs '[]      ys = (ys ~ '[])
  SameShapeAs (x : xs) ys = (ys ~ (Head ys : Tail ys))

type family AllEqF (xs :: [a]) (ys :: [a]) :: Constraint where
  AllEqF '[]      '[]      = ()
  AllEqF (x : xs) (y : ys) = (x ~ y, AllEq xs ys)

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

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

Expected behavior

I would expect the program to be accepted.

Environment

• GHC version used: 9.2.0.20210406, built locally on my machine from the ghc-9.2 branch at commit d197fb3d

Optional:

• Operating System: Linux (NixOS)
• System Architecture: x86_64