Can't prove unique refinement type for filter function

Question

I am following the LH tutorial and am stuck at the excersise to refine the type of the filter function in a way that, if called with a list with unique elements, the output is also a unique list with unique elements.

This is the code I am working with:

import Data.Set hiding (insert, partition, filter, split, elems)

{-@ measure elts @-}
elts        :: (Ord a) => [a] -> Set a
elts []     = empty
elts (x:xs) = singleton x `union` elts xs

{-@ measure unique @-}
unique        :: (Ord a) => [a] -> Bool
unique []     = True
unique (x:xs) = unique xs && not (member x (elts xs))

{-@ filter' :: (a -> Bool) -> xs:[a] -> { l:[a] | unique xs => unique l } @-}
filter' _ []   = []
filter' f (x:xs)
  | f x       = x : xs'
  | otherwise = xs'
  where
    xs'       = filter' f xs

however, when let LH prove it the following error is thrown by LH:

filter.hs:16:17-23: Error: Liquid Type Mismatch

 16 |   | f x       = x : xs'
                      ^^^^^^^

   Inferred type
     VV : {v : [a] | tail v == xs'
                     && head v == x
                     && listElts v == Set_cup (Set_sng x) (listElts xs')
                     && len v == 1 + len xs'
                     && Main.elts v == Set_cup (Set_sng x) (Main.elts xs')
                     && (Main.unique v <=> Main.unique xs'
                                           && not (Set_mem x (Main.elts xs')))
                     && len v >= 0}

   not a subtype of Required type
     VV : {VV : [a] | Main.unique ?a => Main.unique VV}

   In Context
     xs : {v : [a] | len v >= 0}

     xs' : {v : [a] | (Main.unique xs => Main.unique v)
                      && len v >= 0}

     x : a

     ?a : {?a : [a] | len ?a >= 0}

I have already tried to specify it differently, using an if in the refinement and by using different refinement types, but none of it seems to work...

can you please point me in the right direction? I am still having a hard time understanding the error messages. As I understand it, the inferred type contains the information that it is uniqe if xs' is unique, so in my opinion, this should be a subtype of the required one.

Answer 1

sorry for the delay, I just saw this! (I tend to monitor the slack channel more closely.) The error message basically says that LH cannot prove that the output list x:xs' will indeed be unique. Specifically, LH has no way to know that x is not already an element of xs'.

Now, why is x not an element of xs'? Because

(1) x is not an element of xs AND (2) xs' is a subset of the values of xs

LH knows the first property if the input list is unique.

But it does not know the second. So if you add that to the output of filter that would help.

[This is an excellent question by the way; I will update the tutorial with a hint]