Add occurs check at dependent eliminator

[leodemoura]

The occurs check is missing, and prevents Lean from elaborating the following example

namespace STLC

abbrev Var := Char

inductive type where
  | base  : type
  | arrow : type → type → type

inductive term where
  | var : Var → term
  | lam : Var → type → term → term
  | app : term → term → term

def ctx := List (Var × type)

open type term in
inductive typing : ctx → term → type → Prop where
  | var  : typing ((x, A) :: Γ) (var x) A -- simplified
  | arri : typing ((x, A) :: Γ) M B → typing Γ (lam x A M) (arrow A B)
  | arre : typing Γ M (arrow A B) → typing Γ N A → typing Γ (app M N) B

open type term in
theorem no_δ : ¬ ∃ A B, typing nil (lam x A (app (var x) (var x))) (arrow A B) :=
  fun h => match h with
  | Exists.intro A (Exists.intro B h) => match h with
    | typing.arri h => match h with
      | typing.arre (A := T) h₁ h₂ => match h₂ with
        | typing.var => nomatch h₁ -- Fail here

namespace STLC

The nomatch h₁ fails to detect that arrow A B = A has no solutions.

[digama0]

While this would be nice to have, it looks low priority to me. noConfusion style proofs can't handle occurs check reasoning, so you would need a custom inductive proof on the spot. The usual way is to use Nat.lt transitivity with a sizeof function to argue that sizeof A < sizeof (arrow A B), but this has lots of limitations in the dependent type situation and generally goes quite a bit beyond what the equation compiler normally needs to do. Note also that the theorem is false for inductive predicates: if type was a Prop then arrow A B = A would be true. I would not really expect nomatch to be able to do this proof.