Is it reasonable to allow the type of a λ/∀-bound variable to refer to itself? Usually, in Pure Type Systems, the type of a λ/∀-bound variable is only accessible on its body. That is, on λ (X : A) -&gt; B, X is free inside A and bound in B. But what if X was also bound in A? The typing rules should be updated accordingly, i.e., instead of:

$$ \frac{Γ \vdash A : * \quad Γ, x : A \vdash B : *}{Γ \vdash ∀ (x : A) \rightarrow B : *}$$
$$ \frac{Γ \vdash f : ∀ (x : A) \rightarrow B \quad Γ \vdash a : A}{Γ \vdash f a : [a/x]B}$$

we'd have:

$$ \frac{Γ, x : A \vdash A : * \quad Γ, x : A \vdash B : *}{Γ \vdash ∀ (x : A) \rightarrow B : *}$$
$$ \frac{Γ \vdash f : ∀ (x : A) \rightarrow B \quad Γ \vdash a : [a/x]A}{Γ \vdash f a : [a/x]B}$$

In other words, on the ∀ (x : A) -&gt; B case, in order to infer the type of A, we extend the context with x : A, which is possible, because we know the value of A. On the application case f a with f : ∀ (x : A) -&gt; B, we substitute x by a in A before checking for equality. I have never seen such an approach, though. My question is: was this explored before? If so, is there a name for it so I can look up? If not, is there an obvious reason for it to be undesirable?

(The reason I initially asked this question is I've previously asked if it is possible to implement a halting definition of ind on the calculus of constructions with equi-recursion. I've noticed one can do so in a setting with mutually recursive definitions, as long as we also allow a λ/∀-bound variable to refer to itself on its type. Here is an example.)
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)