Warn when names in a single claim / declaration shadow each other

[ohad]

Steps to Reproduce

record Bar (a : Type) where
  constructor MkBar
  a : Nat

Expected Behavior

Depends on language design. Either:

• type-check fine, and be equivalent to the alpha-converted code that type-checks fine:

record Bar (b : Type) where
  constructor MkBar
  a : Nat

• Report a warning that the field named a shadows an earlier argument called a.

Observed Behavior

- + Errors (1)
 `-- (Interactive) line 1 col 0:
     While processing constructor MkBar. When unifying:
         Nat
     and:
         Type
     Mismatch between: Nat and Type.