content: -- TAG: local
  -- tests local-var annotations; complicated by GHC adding TWO `go` binders (nested),
  -- where picking the WRONG one to attach to the annotation yields an LH-GHC-mismatch.
  -- [NOTE:] `Resolve.makeLocalVars` 
  
  module Uniques (uniques) where
  
  import qualified Data.Set as S 
  
  -----------------------------------------------------------------------------------
  -- | Code 
  -----------------------------------------------------------------------------------
  {-@ uniques :: (Eq a) => xs:_ -> {v:ListE a xs | noDups v} @-}
  uniques :: (Eq a) => [a] -> [a]
  uniques xs = go xs []
    where
      {-@ go :: (Eq a) => xs:_ -> acc:_ -> {v:ListU a acc xs | _ } @-}
      go (x:xs) acc 
            | x `isIn` acc = go xs acc     
            | otherwise    = go xs (x:acc)
      go [] acc        = acc 
  
  {-@ isIn:: (Eq a) => x:a -> ys:[a] -> {v:Bool | v = S.member x (S.listElts ys)} @-}
  isIn:: (Eq a) => a -> [a] -> Bool
  isIn _ []     = False 
  isIn x (y:ys) = x == y || isIn x ys
  
  -----------------------------------------------------------------------------------
  -- | Specification 
  -----------------------------------------------------------------------------------
  {-@ measure noDups @-}
  noDups :: (Ord a) => [a] -> Bool
  noDups []     = True 
  noDups (x:xs) = noDups xs && not (S.member x (S.fromList xs)) 
  
  {-@ type ListE a X   = {v:[a] | S.listElts v = S.listElts X} @-}
  {-@ type ListU a X Y = {v:[a] | S.listElts v = S.union (S.listElts X) (S.listElts Y)} @-}
  