模式匹配并非详尽无遗 液体类型不匹配

Question

你好，我是 Haskell 新手，我正在尝试向这两个函数添加 Liquid Haskell 注释。

c :: Int
c = 2

{-@ rotateRev :: r:[a] -> f:[a] -> a:[a] -> y:{v:[a] | len v = len r + len f + len a}
@-}
rotateRev :: [a] -> [a] -> [a] -> [a]
rotateRev [] f a = reverse f ++ a
rotateRev (x:r) f a = x : rotateRev r (drop c f) (reverse (take c f) ++ a)

{-@ rotateDrop :: r:[a] -> i:{v:Int | v >= 0} -> f:{v:[a] | len v > i} -> y:{v:[a] | len v = len r + (len f - i)}
@-}
rotateDrop :: [a] -> Int -> [a] -> [a]
rotateDrop r i f
  | i < c = rotateRev r (drop i f) []
  | otherwise = let (x:r') = r in x : rotateDrop r' (i - c) (drop c f)

我在使用rotateRev时没有收到错误，但在使用rotateDrop时却收到此错误。

Liquid Type Mismatch
    .
    The inferred type
      VV : {v : GHC.Prim.Addr# | v == "C:\Users\u\Downloads\project\src\MyLib.hs:61:21-30|x : r'"}
    .
    is not a subtype of the required type
      VV : {VV : GHC.Prim.Addr# | totalityError "Pattern match(es) are non-exhaustive"}
    .
    Constraint id 75typecheck

Liquid Type Mismatch
    .
    The inferred type
      VV : {v : [a] | (not (MyLib.c >= 0) => len v == len f)
                      && (MyLib.c >= 0 => len v == (if len f < MyLib.c then 0 else len f - MyLib.c))
                      && v == ?b
                      && len v >= 0}
    .
    is not a subtype of the required type
      VV : {VV : [a] | len VV > i - MyLib.c}
    .
    in the context
      MyLib.c : GHC.Types.Int
       
      ?b : {?b : [a] | (not (MyLib.c >= 0) => len ?b == len f)
                       && (MyLib.c >= 0 => len ?b == (if len f < MyLib.c then 0 else len f - MyLib.c))
                       && len ?b >= 0}
       
      f : {f : [a] | len f > i
                     && len f >= 0}
       
      i : {i : GHC.Types.Int | i >= 0}
    Constraint id 69

第二个错误与此相关（drop c f）

我觉得我错过了一些明显的东西。

Answer 1

您有一个非详尽的模式匹配。当你写的时候

  let (x:r') = r in  

您正在对列表进行模式匹配，并且此处缺少空列表情况。