Type class resolution as a (partial) decision procedure

vc.idr

  -- Idris type classes actually take any kind of value as a parameter,
  -- we're not restricted to Sets or parameterised Sets.
  
  -- So we actually have 'value classes'. It seems we can use type class
  -- resolution to make rudimentary decision procedures, then:
  
  using (xs : List a)
    data Elem : a -> List a -> Set where
         Here  : Elem x (x :: xs)
         There : Elem x xs -> Elem x (y :: xs)

  -- TODO: Would be nice if the 'a' could be implicit 
  class IsElem a (x : a) (xs : List a) where
        isElem : Elem x xs
  
  instance IsElem a x (x :: xs) where
        isElem = Here
  
  instance IsElem a x xs => IsElem a x (y :: xs) where
        isElem = There isElem
  
  foo : Elem 4 [1,2,3,4,5,6,7]
  foo = isElem
  
  bar : IsElem Int x xs => Elem x (1 :: 2 :: 3 :: xs)
  bar = isElem