入門 LiquidHaskell p.22 drop の注釈付き実装の検査

Setup.hs

環境
====

- CentOS Linux release 7.4.1708 (Core)
- https://github.com/ucsd-progsys/liquidhaskell.git (commit:16307c7403ba1aeeef9205b414785d36e93a402b)
- stack setup && stack install (GHC 8.2.1)

ログ
====

::
$ liquid Setup.hs
LiquidHaskell Copyright 2013-17 Regents of the University of California. All Rights Reserved.


**** DONE:  A-Normalization ****************************************************


**** DONE:  Extracted Core using GHC *******************************************


**** DONE:  Transformed Core ***************************************************

Working 100% [=================================================================]

**** DONE:  annotate ***********************************************************


**** RESULT: UNSAFE ************************************************************


Setup.hs:29:23-37: Error: Liquid Type Mismatch

 29 |   | otherwise = drop (n - 1) xs
                            ^^^^^^^^^^^^^^^

   Inferred type
     VV : {v : [a] | Setup.length v == Setup.length v - ?c
                     && Setup.length v >= 0
                     && len v >= 0}

   not a subtype of Required type
     VV : {VV : [a] | Setup.length VV == Setup.length VV - ?b}

   In Context
     ?c : {?c : Int | ?c == ?b - ?a}

     ?b : {?b : Int | ?b >= 0}

     ?a : {?a : Int | ?a == (1 : int)}
$ cat Setup.hs
module Setup where

import Prelude hiding (length, take, drop)
import Language.Haskell.Liquid.ProofCombinators

{-@ measure length @-}
{-@ length :: [a] -> Nat @-}
length :: [a] -> Int
length []     = 0
length (_:xs) = 1 + length xs

{-@ type ListLn a N = { xs:[a] | length xs == N } @-}
{-@ type ListGE a N = { xs:[a] | length xs >= N } @-}

{-
{-@ take :: n:Nat -> xs:ListGE a n -> ListLn a n @-}
take :: Int -> [a] -> [a]
take 0      []  = []
take n (x : xs)
        | n == 0    = []
        | otherwise = x : take (n - 1) xs
-}

{-@ drop :: n:Nat -> xs:ListGE a n -> ListLn a { length xs - n } @-}
drop :: Int -> [a] -> [a]
drop 0 [] = []
drop n (x : xs)
        | n == 0    = x : xs
        | otherwise = drop (n - 1) xs
$