Typechecking regression in HEAD involving Givens

The following program, whose only dependency is the ghc-typelits-knownnat type-checking plugin, compiles with GHC 9.12 but no longer compiles with HEAD. @Mikolaj reports that the regression was introduced in ab77fc8c.

{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE ViewPatterns #-}

module T25933 where

import Data.Kind (Type)
import GHC.TypeNats (Nat, SNat, KnownNat, type (+))

type Delta :: [Nat] -> Type
data Delta ns where
  DeltaAppendS
    :: forall m n sh
    .  Delta (m ': sh)
    -> Delta (n ': sh)
    -> Delta ((m + n) ': sh)

data FullShapeTK y where
  FTKS :: SNats sh -> FullShapeTK x -> FullShapeTK sh

ftkDelta :: Delta y -> FullShapeTK y
ftkDelta (DeltaAppendS a b)
  | FTKS (m :$$ sh) x <- ftkDelta a
  , FTKS (n :$$ _ ) _ <- ftkDelta b
  = FTKS (snatPlus m n :$$ sh) x

pattern (:$$)
  :: forall {sh1}.
     forall n sh. (KnownNat n, (n : sh) ~ sh1)
  => SNat n -> SNats sh -> SNats sh1
pattern i :$$ shl <- (uncons -> Just (Uncons i shl))
  where i :$$ shl = (i ::$ shl)
infixr 3 :$$

type SNats :: [Nat] -> Type
data SNats sh where
  ZS :: SNats '[]
  (::$) :: forall n sh. KnownNat n => SNat n -> SNats sh -> SNats (n : sh)
infixr 3 ::$

data Uncons sh1 where
  Uncons
    :: forall n sh sh1
    .  (KnownNat n, (n : sh) ~ sh1)
    => SNat n -> SNats sh -> Uncons sh1
uncons :: SNats sh1 -> Maybe (Uncons sh1)
uncons (x ::$ sh') = Just (Uncons x sh')
uncons ZS = Nothing

snatPlus :: SNat n -> SNat m -> SNat (n + m)
snatPlus n m = error "doesn't matter"

The error occurs when typechecking the occurrence of :$$ in the RHS of the match in ftkDelta:

Could not deduce `KnownNat (m + n)' arising from a use of `:$$'