feat: add hygienicIntro option

@Kha `hygienicIntro` is true by default. `hygienicIntro == false` is
the Lean3 behavior. If we find `hygienicIntro` too inconvenient in
practice, we set the default to false.

src/Lean/Meta/Tactic/Intro.lean

@@ -9,7 +9,7 @@ namespace Lean
 namespace Meta
 
 @[specialize]
-private partial def introNImpAux {σ} (mvarId : MVarId) (mkName : LocalContext → Name → σ → Name × σ)
+private partial def introNImpAux {σ} (mvarId : MVarId) (mkName : LocalContext → Name → σ → MetaM (Name × σ))
     : Nat → LocalContext → Array Expr → Nat → σ → Expr → MetaM (Array Expr × MVarId)
 | 0, lctx, fvars, j, _, type =>
   let type := type.instantiateRevRange j fvars.size fvars;
@@ -27,7 +27,7 @@ private partial def introNImpAux {σ} (mvarId : MVarId) (mkName : LocalContext
   let type   := type.headBeta;
   let val    := val.instantiateRevRange j fvars.size fvars;
   fvarId ← mkFreshId;
-  let (n, s) := mkName lctx n s;
+  (n, s) ← mkName lctx n s;
   let lctx   := lctx.mkLetDecl fvarId n type val;
   let fvar   := mkFVar fvarId;
   let fvars  := fvars.push fvar;
@@ -36,7 +36,7 @@ private partial def introNImpAux {σ} (mvarId : MVarId) (mkName : LocalContext
   let type   := type.instantiateRevRange j fvars.size fvars;
   let type   := type.headBeta;
   fvarId ← mkFreshId;
-  let (n, s) := mkName lctx n s;
+  (n, s) ← mkName lctx n s;
   let lctx   := lctx.mkLocalDecl fvarId n type c.binderInfo;
   let fvar   := mkFVar fvarId;
   let fvars  := fvars.push fvar;
@@ -51,7 +51,7 @@ private partial def introNImpAux {σ} (mvarId : MVarId) (mkName : LocalContext
       else
         throwTacticEx `introN mvarId "insufficient number of binders"
 
-@[specialize] private def introNImp {σ} (mvarId : MVarId) (n : Nat) (mkName : LocalContext → Name → σ → Name × σ) (s : σ) : MetaM (Array FVarId × MVarId) :=
+@[specialize] private def introNImp {σ} (mvarId : MVarId) (n : Nat) (mkName : LocalContext → Name → σ → MetaM (Name × σ)) (s : σ) : MetaM (Array FVarId × MVarId) :=
 withMVarContext mvarId $ do
   checkNotAssigned mvarId `introN;
   mvarType ← getMVarType mvarId;
@@ -59,13 +59,38 @@ withMVarContext mvarId $ do
   (fvars, mvarId) ← introNImpAux mvarId mkName n lctx #[] 0 s mvarType;
   pure (fvars.map Expr.fvarId!, mvarId)
 
-private def mkAuxNameImp (preserveBinderNames : Bool) (lctx : LocalContext) (binderName : Name) : List Name → Name × List Name
-| []         => (if preserveBinderNames then binderName else lctx.getUnusedName binderName, [])
-| n :: rest  => (if n != "_" then n else if preserveBinderNames then binderName else lctx.getUnusedName binderName, rest)
+def hygienicIntroDef := true
 
-def introNCore (mvarId : MVarId) (n : Nat) (givenNames : List Name) (preserveBinderNames : Bool) : MetaM (Array FVarId × MVarId) :=
+def getHygienicIntro : MetaM Bool := do
+o ← getOptions;
+pure $ o.get `hygienicIntro hygienicIntroDef
+
+@[init] def registerHygienicIntro : IO Unit :=
+registerOption `hygienicIntro { defValue := hygienicIntroDef, group := "tactic", descr := "make sure 'intro'-like tactics are hygienic" }
+
+private def mkAuxNameImp (preserveBinderNames : Bool) (hygienic : Bool) (lctx : LocalContext) (binderName : Name) : List Name → MetaM (Name × List Name)
+| []         =>
+  if preserveBinderNames then
+    pure (binderName, [])
+  else if hygienic then do
+    binderName ← Core.mkFreshUserName binderName;
+    pure (binderName, [])
+  else
+    pure (lctx.getUnusedName binderName, [])
+| n :: rest  =>
+  if n != "_" then pure (n, rest)
+  else if preserveBinderNames then
+    pure (binderName, rest)
+  else if hygienic then do
+    binderName ← Core.mkFreshUserName binderName;
+    pure (binderName, rest)
+  else
+    pure (lctx.getUnusedName binderName, rest)
+
+def introNCore (mvarId : MVarId) (n : Nat) (givenNames : List Name) (preserveBinderNames : Bool) : MetaM (Array FVarId × MVarId) := do
+hygienic ← getHygienicIntro;
 if n == 0 then pure (#[], mvarId)
-else introNImp mvarId n (mkAuxNameImp preserveBinderNames) givenNames
+else introNImp mvarId n (mkAuxNameImp preserveBinderNames hygienic) givenNames
 
 abbrev introN (mvarId : MVarId) (n : Nat) (givenNames : List Name := []) : MetaM (Array FVarId × MVarId) :=
 introNCore mvarId n givenNames false

tests/lean/hygienicIntro.lean

@@ -0,0 +1,47 @@
+new_frontend
+
+set_option hygienicIntro false in
+theorem ex1 {a p q r : Prop} : p → (p → q) → (q → r) → r := by
+intro _ h1 h2;
+apply h2;
+apply h1;
+exact a_1 -- Bad practice, using name generated by `intro`.
+
+theorem ex2 {a p q r : Prop} : p → (p → q) → (q → r) → r := by
+intro _ h1 h2;
+apply h2;
+apply h1;
+exact a_1 -- error "unknown identifier"
+
+theorem ex3 {a p q r : Prop} : p → (p → q) → (q → r) → r := by
+intro _ h1 h2;
+apply h2;
+apply h1;
+assumption
+
+example {p q : Prop} (h₁ : p → q) (h₂ : p ∨ q) : q := by
+cases h₂;
+{ apply h₁; exact h }; -- error "unknown identifier"
+exact h
+
+set_option hygienicIntro false in
+example {p q : Prop} (h₁ : p → q) (h₂ : p ∨ q) : q := by
+cases h₂;
+{ apply h₁; exact h }; -- hygiene is disabled
+exact h
+
+-- Hygienic versions
+example {p q : Prop} (h₁ : p → q) (h₂ : p ∨ q) : q := by
+cases h₂ with
+| inl h => apply h₁; exact h
+| inr h => exact h
+
+example {p q : Prop} (h₁ : p → q) (h₂ : p ∨ q) : q := by
+cases h₂;
+{ apply h₁; assumption };
+assumption
+
+example {p q : Prop} (h₁ : p → q) (h₂ : p ∨ q) : q := by
+match h₂ with
+| Or.inl _ => apply h₁; assumption
+| Or.inr h => exact h

tests/lean/hygienicIntro.lean.expected.out

@@ -0,0 +1,2 @@
+hygienicIntro.lean:14:6: error: unknown identifier 'a_1'
+hygienicIntro.lean:24:18: error: unknown identifier 'h'

tests/lean/match1.lean.expected.out

@@ -13,7 +13,7 @@
 match1.lean:82:0: error: type mismatch during dependent match-elimination at pattern variable 'w' with type
   VecPred P Vec.nil
 expected type
-  VecPred P tail
+  VecPred P tail✝
 [false, true, true]
 match1.lean:113:0: error: dependent match elimination failed, inaccessible pattern found 
   .(j + j)