fix: scope and improve error message

src/Lean/Message.lean

@@ -183,9 +183,12 @@ end MessageLog
 def MessageData.nestD (msg : MessageData) : MessageData :=
 MessageData.nest 2 msg
 
-def indentExpr (msg : MessageData) : MessageData :=
+def indentD (msg : MessageData) : MessageData :=
 MessageData.nestD (Format.line ++ msg)
 
+def indentExpr (e : Expr) : MessageData :=
+indentD e
+
 namespace KernelException
 
 private def mkCtx (env : Environment) (lctx : LocalContext) (opts : Options) (msg : MessageData) : MessageData :=

src/Lean/Meta/Match/Match.lean

@@ -550,18 +550,22 @@ match p.vars with
       newAlts ← newAlts.filterMapM fun alt => match alt.patterns with
         | Pattern.ctor _ _ _ fields :: ps  => pure $ some { alt with patterns := fields ++ ps }
         | Pattern.var fvarId :: ps         => expandVarIntoCtor? { alt with patterns := ps } fvarId subgoal.ctorName
-        | Pattern.inaccessible e :: ps     => do
+        | p@(Pattern.inaccessible e) :: ps => do
           trace! `Meta.Match.match ("inaccessible in ctor step " ++ e);
-          e ← whnfD e;
-          match e.constructorApp? env with
-          | some (ctorVal, ctorArgs) => do
-            if ctorVal.name == subgoal.ctorName then
-              let fields := ctorArgs.extract ctorVal.nparams ctorArgs.size;
-              let fields := fields.toList.map Pattern.inaccessible;
-              pure $ some { alt with patterns := fields ++ ps }
-            else
-              pure none
-          | _ => pure none
+          withExistingLocalDecls alt.fvarDecls do
+            -- Try to push inaccessible annotations.
+            e ← whnfD e;
+            match e.constructorApp? env with
+            | some (ctorVal, ctorArgs) => do
+              if ctorVal.name == subgoal.ctorName then
+                let fields := ctorArgs.extract ctorVal.nparams ctorArgs.size;
+                let fields := fields.toList.map Pattern.inaccessible;
+                pure $ some { alt with patterns := fields ++ ps }
+              else
+                pure none
+            | _ => throwErrorAt alt.ref $
+              "dependent match elimination failed, inaccessible pattern found " ++ indentD p.toMessageData ++
+              Format.line ++ "constructor expected"
         | _                                => unreachable!;
       pure { mvarId := subgoal.mvarId, vars := newVars, alts := newAlts, examples := examples }
 

tests/lean/match1.lean

@@ -85,3 +85,38 @@ axiom someNat : Nat
 
 noncomputable def f2 (x : Nat) := -- must mark as noncomputable since it uses axiom `someNat`
 x + someNat
+
+inductive Parity : Nat -> Type
+| even (n) : Parity (n + n)
+| odd  (n) : Parity (Nat.succ (n + n))
+
+axiom nDiv2 (n : Nat)     : n % 2 = 0 → n = n/2 + n/2
+axiom nDiv2Succ (n : Nat) : n % 2 ≠ 0 → n = Nat.succ (n/2 + n/2)
+
+def parity (n : Nat) : Parity n :=
+if h : n % 2 = 0 then
+  Eq.ndrec (Parity.even (n/2)) (nDiv2 n h).symm
+else
+  Eq.ndrec (Parity.odd (n/2)) (nDiv2Succ n h).symm
+
+partial def natToBin : (n : Nat) → List Bool
+| 0 => []
+| n => match n, parity n with
+  | _, Parity.even j => false :: natToBin j
+  | _, Parity.odd  j => true  :: natToBin j
+
+#eval natToBin 6
+
+partial def natToBinBad (n : Nat) : List Bool :=
+match n, parity n with
+| 0, _             => []
+| _, Parity.even j => false :: natToBin j
+| _, Parity.odd  j => true  :: natToBin j
+
+partial def natToBin2 (n : Nat) : List Bool :=
+match n, parity n with
+| _, Parity.even 0 => []
+| _, Parity.even j => false :: natToBin j
+| _, Parity.odd  j => true  :: natToBin j
+
+#eval natToBin2 6

tests/lean/match1.lean.expected.out

@@ -14,3 +14,8 @@ match1.lean:82:0: error: type mismatch during dependent match-elimination at pat
   VecPred P Vec.nil
 expected type
   VecPred P tail
+[false, true, true]
+match1.lean:113:0: error: dependent match elimination failed, inaccessible pattern found 
+  .(j+j)
+constructor expected
+[false, true, true]