typelevel scala: ensure single instance of case class per constructor argument by typing alone?

Question

Let's say I have a trait and case classes corresponding to an expression language for a dsl.

sealed trait Expr[T]

case class Ident[T]() extends Expr[T]

case class Operator1[T](e1: Expr[T], e2: Expr[T]) extends Expr[T]
...
...

And that I also have a case class used to assign an expression to an identifier:

sealed trait DefLike[T]

case class Def[T](id: Ident[T], e: Expr[T]) extends DefLike[T]

case class Free[T](id:Ident[T]) extends DefLike[T]

The DSL is for a declarative language in which all identifiers can be given at most one definition.

So this would be accepted:

for { 
x <- Ident[Int]
y <- Ident[Int]
y_e <- Mult(Const(3), x) } yield Free(x) :: Def(y, y_e) :: Nil

However this would be forbidden:

for { 
x <- Ident[Int]
y <- Ident[Int]
y_e <- Mult(Const(3), x) } yield Free(x) :: Free(y) :: Def(x, x) :: Def(y, y_e) :: Nil

I also need to make sure that the sequence of definition is topoligically ordered, all of this at compile-time.

I was thinking of using shapeless Nat to assign an extra and unique type parameter to each identifier using some sort of wrapper function:

trait Expr[T] { type N <: Nat }
class Ident[T, M <: Nat]() extends Expr[T, M <: Nat] { type N = M }
...
...

object Builder {
   var i: Int = 0 
   def ident[T] = {i++; new Ident[T,intToNat(i)]}
}

trait DefLike[T, N <: Nat]
case class Def[T, N <: Nat](id: Ident[T,N], e: Expr[T])(implicit ev: GreaterThan[N, e.N]) extends DefLike[T, N]
case class Free[T, N <: Nat](id: Ident[T,N]) extends DefLike[T, N]

And then use some sort of type-level hackery to make the following work:

• The Nat type N assigned to any expression is the Max of the Nat types of its subexpressions.
• unique Nat Types are assigned to identifiers (doing it with a wrapper as above)
• an implicity GreaterThan[N, e.N] holds for Def[T, N](id, e): the Nat type of the defining expression is less than that of the identifier being defined (ensures topological ordering of definitions)
• define a type level constraint using type-level fold or type-level map to ensure that no two DefLike[T, N <: Nat] have the same N in a list of DefLike

Does it seem to be a good case for Nat ? How can I approach the fold over a type level list of types to detect type doublons? Thanks,