From 6714601ee4a123fef0f6ff3e44f01086ba78dfce Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 16 Mar 2026 23:43:51 -0700 Subject: [PATCH] fix: remove accidental type monomorphism in `Id.run_seqLeft` (#12936) This PR fixes `Id.run_seqLeft` and `Id.run_seqRight` to apply when the two monad results are different. --- src/Init/Control/Lawful/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/Control/Lawful/Basic.lean b/src/Init/Control/Lawful/Basic.lean index fe66c756fe..8382809f04 100644 --- a/src/Init/Control/Lawful/Basic.lean +++ b/src/Init/Control/Lawful/Basic.lean @@ -254,8 +254,8 @@ instance : LawfulMonad Id := by @[simp, grind =] theorem run_bind (x : Id α) (f : α → Id β) : (x >>= f).run = (f x.run).run := rfl @[simp, grind =] theorem run_pure (a : α) : (pure a : Id α).run = a := rfl @[simp, grind =] theorem pure_run (a : Id α) : pure a.run = a := rfl -@[simp] theorem run_seqRight (x y : Id α) : (x *> y).run = y.run := rfl -@[simp] theorem run_seqLeft (x y : Id α) : (x <* y).run = x.run := rfl +@[simp] theorem run_seqRight (x : Id α) (y : Id β) : (x *> y).run = y.run := rfl +@[simp] theorem run_seqLeft (x : Id α) (y : Id β) : (x <* y).run = x.run := rfl @[simp] theorem run_seq (f : Id (α → β)) (x : Id α) : (f <*> x).run = f.run x.run := rfl end Id