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 ab77fc8c7adebd610aa0bd99d653f9a6cc78a374.
```hs
{-# 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 `:$$'
```
issue