> Have you seen languages like DML (let's you capture linear arithmetic properties only and automates the proof of these)?

Yes. But what I have in mind is a little bit more ambitious. I want dependent types restricted to be parameterized by syntactic values (in the sense of ML's value restriction) of what Standard ML calls `eqtype`s. For example, correctly balanced red-black trees would be:

    (* clearly eqtypes *)
    datatype Color = R' | B'
    datatype Nat = Z | S : Nat -> Nat
    
    datatype Tree =
      | Empty : Tree (B', Z, 'a)
      | R : Tree (B', 'h, 'a) * 'a * Tree (B', 'h, 'a) -> Tree (R', 'h, 'a)
      | B : Tree ('c, 'h, 'a) * 'a * Tree ('c, 'h, 'a) -> Tree (B', S 'h, 'a)