Is it reasonable to allow the type of a λ/∀-bound variable to refer to itself?
I have not seen this in a dependently-typed setting, but a similar notion is fairly well-known in weaker systems (e.g. System F) with subtyping, under the term "F-bounded quantification". This pops up prominently in type systems for object-oriented programming languages, which typically are heavy on (equi-) type recursion. This notion was originally introduced by this paper.

A standard use case is expressing forms of "binary methods" that need to be covariant in their argument types. For example, in those languages you see interface types like

interface Ordered&lt;T&gt; { less(x : T) : Bool }


with subtypes like

class Int extends Ordered&lt;Int&gt; { ... }


and usage patterns

class Queue&lt;T extends Ordered&lt;T&gt;&gt; { ... }


or

sort&lt;T extends Ordered&lt;T&gt;&gt;(array : Array&lt;T&gt;) : Array&lt;T&gt;


and so on. In the more type-theoretical rendering of System F-sub with F-bounded quantification and records these could be expressed as

Ordered = λ(T &lt;: Top). {less : T → Bool}
Int &lt;: Ordered(Int)
Queue = λ(T &lt;: Ordered(T)). {...}
sort : ∀(T &lt;: Ordered(T)). Array(T) → Array(T)