From fbd8224b4dcda068e3fc93f0b61990ccfec96a39 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 27 May 2022 11:23:51 -0700 Subject: [PATCH] fix: allow recursive occurrences in binder types at `WF/PackDomain.lean` fixes #1171 --- .../Elab/PreDefinition/WF/PackDomain.lean | 22 ++++++++++++------- tests/lean/run/1171.lean | 13 +++++++++++ 2 files changed, 27 insertions(+), 8 deletions(-) create mode 100644 tests/lean/run/1171.lean diff --git a/src/Lean/Elab/PreDefinition/WF/PackDomain.lean b/src/Lean/Elab/PreDefinition/WF/PackDomain.lean index 2bbae325f8..9f968200ca 100644 --- a/src/Lean/Elab/PreDefinition/WF/PackDomain.lean +++ b/src/Lean/Elab/PreDefinition/WF/PackDomain.lean @@ -131,14 +131,20 @@ where visit (e : Expr) : MonadCacheT ExprStructEq Expr MetaM Expr := do checkCache { val := e : ExprStructEq } fun _ => Meta.withIncRecDepth do match e with - | Expr.lam .. => lambdaTelescope e fun xs b => do mkLambdaFVars (usedLetOnly := false) xs (← visit b) - | Expr.letE n t v b _ => withLetDecl n t (← visit v) fun x => do mkLambdaFVars (usedLetOnly := false) #[x] (← visit (b.instantiate1 x)) - | Expr.forallE .. => forallTelescope e fun xs b => do mkForallFVars (usedLetOnly := false) xs (← visit b) - | Expr.proj n i s .. => return mkProj n i (← visit s) - | Expr.mdata d b _ => return mkMData d (← visit b) - | Expr.app .. => visitApp e - | Expr.const .. => visitApp e - | e => return e, + | Expr.lam n d b c => + withLocalDecl n c.binderInfo (← visit d) fun x => do + mkLambdaFVars (usedLetOnly := false) #[x] (← visit (b.instantiate1 x)) + | Expr.forallE n d b c => + withLocalDecl n c.binderInfo (← visit d) fun x => do + mkForallFVars (usedLetOnly := false) #[x] (← visit (b.instantiate1 x)) + | Expr.letE n t v b c => + withLetDecl n (← visit t) (← visit v) fun x => do + mkLambdaFVars (usedLetOnly := false) #[x] (← visit (b.instantiate1 x)) + | Expr.proj n i s .. => return mkProj n i (← visit s) + | Expr.mdata d b _ => return mkMData d (← visit b) + | Expr.app .. => visitApp e + | Expr.const .. => visitApp e + | e => return e, visitApp (e : Expr) : MonadCacheT ExprStructEq Expr MetaM Expr := e.withApp fun f args => do let args ← args.mapM visit if let some funIdx := isAppOfPreDef? f then diff --git a/tests/lean/run/1171.lean b/tests/lean/run/1171.lean new file mode 100644 index 0000000000..d8a90e5d6c --- /dev/null +++ b/tests/lean/run/1171.lean @@ -0,0 +1,13 @@ +def Nat.hasDecEq: (a: Nat) → (b: Nat) → Decidable (Eq a b) +| 0, 0 => isTrue rfl +| n+1, 0 +| 0, n+1 => isFalse Nat.noConfusion +| n+1, m+1 => + match h:hasDecEq n m with -- it works without `h:` + | isTrue heq => isTrue (heq ▸ rfl) + | isFalse hne => isFalse (Nat.noConfusion · (λ heq => absurd heq hne)) +termination_by _ a b => (a, b) + +set_option pp.proofs true +#print Nat.hasDecEq +#print Nat.hasDecEq._unary