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