public export
data Uni : a -> UniqueType where
    U : a -> Uni a

export
data UComparator : Nat -> a -> UniqueType where
    MkComparator : (allowedUses : Nat) -> (comp : (a -> a -> Bool)) -> UComparator allowedUses a

interface EfficientLookup (c : UniqueType) where
    keyType : c ->  Type
    valType : c ->  Type
    size : c ->  Nat
    lookupImpl : (coll : c) -> (UComparator (size coll) (keyType coll)) -> (keyType coll) -> Uni (valType coll)

export
total compareOnce : {n : Nat} -> {a : Type} -> UComparator (S n) a  -> a -> a -> UPair Bool (UComparator n a)
compareOnce (MkComparator (S rem) comp) a1 a2 = (comp a1 a2,  MkComparator rem comp)