Constraints.idr

module Data.List.Constraints

import Data.Vect

data NotElem : a -> List a -> Type where
  NotHere  : NotElem x []
  NotThere : Eq ty => {x,y : ty}  -> {auto prf : x /= y = True} -> NotElem x xs -> NotElem x (y::xs)


data AllDiff : List a -> Type where
  EmptyCase : AllDiff Nil
  OneCase   : AllDiff [x]
  ManyCase  : NotElem x xs -> AllDiff xs -> AllDiff (x::xs)

data UniqueList : (a : Type) -> List a -> Type where
  Nil : UniqueList ty Nil
  (::) : (x : ty)
      -> (xs : UniqueList ty xs')
      -> {auto prf : NotElem x xs'}
      -> {auto prf : AllDiff (x::xs')}
      -> UniqueList ty (x::xs')

UniqueList' : Type -> Type
UniqueList' ty = Subset (List ty) (\xs => AllDiff xs)

fromList : Eq a
        => (xs : List a)
        -> {auto prf : AllDiff xs}
        -> UniqueList' a
fromList xs {prf} = Element xs prf