Pattern match checker gives contradicting incomplete-patterns and inaccessible-code warnings

I have the following code involving generics-sop:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE BangPatterns #-}

module Cursor where

import Data.Kind
import Data.Word

import qualified GHC.Generics as GHC
import Generics.SOP

import Foreign.Storable
import Foreign.Ptr

import System.IO.Unsafe

data Tree = Leaf Int | Node Tree Tree
  deriving stock (Show, GHC.Generic)
  deriving anyclass Generic

type family (++) (xs :: [k]) (ys :: [k]) :: [k] where
  '[] ++ ys = ys
  (x ': xs) ++ ys = x ': (xs ++ ys)

newtype RCursor (xs :: [Type]) where
  RCursor :: Ptr Word8 -> RCursor xs

newtype RStack (ys :: [Type]) (xs :: [Type]) where
  RStack :: forall ys xs. RCursor (xs ++ ys) -> RStack ys xs

readStorable :: forall x xs. Storable x => RCursor (x ': xs) -> (x, RCursor xs)
readStorable (RCursor ptr) = unsafePerformIO $ do
  x<- peek $ alignPtr (castPtr ptr) (alignment (undefined :: x))
  pure (x, RCursor (ptr `plusPtr` sizeOf x))

readTagged :: forall x xs xss. (Code x ~ xss,SListI xss) => RCursor (x ': xs) -> NS (RStack xs) xss
readTagged (RCursor ptr)= unsafePerformIO $ do
  tag <- peek $ alignPtr (castPtr ptr) (alignment (undefined :: Int))
  let
    ptr' :: Ptr Word8
    ptr' = ptr `plusPtr` sizeOf tag
    loop :: forall ys. Int -> Shape ys -> NS (RStack xs) ys
    loop _ ShapeNil       = error $ "exhausted alternatives in readTag, got " ++ show tag ++ ", expected " ++ show (lengthSList (Proxy @xss))
    loop 0 (ShapeCons _ ) = Z (RStack (RCursor ptr'))
    loop n (ShapeCons xs) = S (loop (n-1) xs)

  pure $ loop tag shape

sumTree :: RCursor (Tree ': xs) -> (Int, RCursor xs)
sumTree = go 0

go :: forall xs. Int -> RCursor (Tree ': xs) -> (Int, RCursor xs)
go !acc cur = case readTagged cur of
  Z (RStack cur) ->
    let (i, cur') = readStorable cur
      in (acc+i, cur')
  S (Z (RStack cur)) ->
    let (acc', cur') = go acc cur
      in go acc' cur'

When compiled with -Winaccessible-code -Wincomplete-patterns -Woverlapping-patterns, it results in the following warning:

src/Cursor.hs:63:15: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In a case alternative: Patterns not matched: S (S _)
   |
63 | go !acc cur = case readTagged cur of
   |               ^^^^^^^^^^^^^^^^^^^^^^...

However, inserting the pattern match S (S (Z (RStack _))) -> undefined results in the following (correct) warnings:

src/Cursor.hs:70:3: warning: [-Woverlapping-patterns]
    Pattern match has inaccessible right hand side
    In a case alternative: S (S (Z (RStack _))) -> ...
   |
70 |   S (S (Z (RStack _))) -> undefined
   |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

src/Cursor.hs:70:9: warning: [-Winaccessible-code]
    • Couldn't match type ‘'[]’ with ‘x2 : xs3’
      Inaccessible code in
        a pattern with constructor:
          Z :: forall k (a :: k -> *) (x :: k) (xs :: [k]).
               a x -> NS a (x : xs),
        in a case alternative
    • In the pattern: Z (RStack _)
      In the pattern: S (Z (RStack _))
      In the pattern: S (S (Z (RStack _)))
   |
70 |   S (S (Z (RStack _))) -> undefined
   |         ^^^^^^^^^^^^

The duplicated warnings are a bit strange, but that is a minor issue. More concerning is the fact that GHC warns about incomplete matches when there are at least 2(!) code paths in the compiler that know that the pattern warned about is impossible.

I've tested this on GHC 8.10.4 and 9.0.1