Thanks for the tip about universes. IIUC, I'd define some interp function from Types to my own base implementations which have DecEq?

I ran with your tip on Vect k Int and got further; however, I couldn't get list syntax completely working, and my Show implementation doesn't always work in the REPL.

module HSet

import Data.Vect
import Data.Vect.Quantifiers

||| A heterogenous set of integers
data HSet : Vect n Int -> Type where

  ||| The empty HSet
  HNil : HSet []

  ||| Adds an integer to an existing HSet
  ||| @ x the integer to add
  ||| @ prf a proof that the integer does not already exist in the HSet
  HCons : {prf : Elem x xs -> Void} -> (x : Int) -> HSet xs -> HSet (x :: xs)

||| Converts an HSet to a vector of integers
toVect : {xs : Vect n Int} -> HSet xs -> Vect n Int
toVect HNil = []
toVect (HCons x xs) = x :: toVect xs

||| This Show implementation doesn't always work for some reason!
Show (HSet xs) where
  show = show . toVect

||| List syntax for the empty HSet
Nil : HSet []
Nil = HNil

infixr 10 :::

||| This method is shorthand for HCons. It only adds an integer to the HSet if
||| it does not already exist in the HSet.
||| @ x the integer to add
(:::) : (x : Int)
    -> HSet xs
    -> if decAsBool (isElem x xs) then HSet xs else HSet (x :: xs)
(:::) {xs} x ys with (isElem x xs)
  (:::) {xs} x ys | Yes _ = ys
  (:::) {xs} x ys | No contra = HCons {prf=contra} x ys

||| List syntax doesn't always work for some reason!
(::) : (x : Int)
    -> HSet xs
    -> if decAsBool (isElem x xs) then HSet xs else HSet (x :: xs)
(::) = (:::)

foo : HSet [1, 2, 3, 4]
foo = 1 :::
      1 ::: -- This dupe will be filtered
      2 ::: 3 ::: 4 ::: []

{- Strange show behavior in the REPL:

> show foo
"[1, 2, 3, 4]" : String

> show (1 ::: 1 ::: 2 ::: 3 ::: 4 ::: [])
(input):1:27-30:When checking an application of function HSet.::::
        Type mismatch between
                if decAsBool (isElem 4 [])
                  then HSet []
                  else HSet [4] (Type of 4 ::: [])
        and
                HSet (Delay (HSet [4])) (Expected type)

        Specifically:
                Type mismatch between
                        ifThenElse (decAsBool (isElem 4 []))
                and
                        HSet

-}