From 7822ee4500ee63c8ac8398a159d140dbf347d36e Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 19 Sep 2025 14:36:47 +0200 Subject: [PATCH] fix: check that compiler does not infer inconsistent types between modules (#10418) This PR fixes a potential miscompilation when using non-exposed type definitions using the module system by turning it into a static error. A future revision may lift the restriction by making the compiler metadata independent of the current module. --- .../Iterators/Combinators/Monadic/ULift.lean | 1 + src/Init/Data/Slice/Array/Iterator.lean | 3 +- src/Init/System/Promise.lean | 8 +-- src/Lean/Compiler/LCNF/Types.lean | 68 ++++++++++++------- src/Lean/Meta/LazyDiscrTree.lean | 2 +- src/Lean/Meta/Tactic/Grind/Types.lean | 1 + src/Std/Sync/Channel.lean | 10 +-- src/Std/Time/Format/Basic.lean | 5 +- src/lake/Lake/Build/Key.lean | 1 + src/lake/Lake/Util/Cli.lean | 1 + tests/lean/run/grind_bintree.lean | 2 +- tests/lean/run/grind_ite.lean | 2 +- tests/pkg/module/Module/Basic.lean | 15 ++++ 13 files changed, 80 insertions(+), 39 deletions(-) diff --git a/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean b/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean index ed6dda19bd..6b22828659 100644 --- a/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean +++ b/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean @@ -19,6 +19,7 @@ universe v u v' u' section ULiftT /-- `ULiftT.{v, u}` shrinks a monad on `Type max u v` to a monad on `Type u`. -/ +@[expose] -- for codegen def ULiftT (n : Type max u v → Type v') (α : Type u) := n (ULift.{v} α) /-- Returns the underlying `n`-monadic representation of a `ULiftT n α` value. -/ diff --git a/src/Init/Data/Slice/Array/Iterator.lean b/src/Init/Data/Slice/Array/Iterator.lean index 2776739fa3..c7f793594b 100644 --- a/src/Init/Data/Slice/Array/Iterator.lean +++ b/src/Init/Data/Slice/Array/Iterator.lean @@ -10,7 +10,7 @@ public import Init.Core public import Init.Data.Slice.Array.Basic import Init.Data.Iterators.Combinators.Attach import Init.Data.Iterators.Combinators.FilterMap -import Init.Data.Iterators.Combinators.ULift +public import Init.Data.Iterators.Combinators.ULift public import Init.Data.Iterators.Consumers.Collect public import Init.Data.Iterators.Consumers.Loop public import Init.Data.Range.Polymorphic.Basic @@ -31,7 +31,6 @@ open Std Slice PRange Iterators variable {shape : RangeShape} {α : Type u} -@[no_expose] instance {s : Subarray α} : ToIterator s Id α := .of _ (PRange.Internal.iter (s.internalRepresentation.start... return .sort u - | .const .. => visitApp type #[] - | .lam n d b bi => - withLocalDecl n bi d fun x => do - let d ← toLCNFType d - let b ← toLCNFType (b.instantiate1 x) - if b.isErased then - return b - else - return Expr.lam n d (b.abstract #[x]) bi - | .forallE .. => visitForall type #[] - | .app .. => type.withApp visitApp - | .fvar .. => visitApp type #[] - | .proj ``Subtype 0 (.const ``IO.RealWorld.nonemptyType []) => - return mkConst ``lcRealWorld - | _ => return mkConst ``lcAny + let res ← go type + if (← getEnv).header.isModule then + -- Under the module system, `type` may reduce differently in different modules, leading to + -- IR-level mismatches and thus undefined behavior. We want to make this part independent of the + -- current module and its view of the environment but until then, we force the user to make + -- involved type definitions exposed by checking whether we would infer a different type in the + -- public scope. We ignore failed inference in the public scope because it can easily fail when + -- compiling private declarations using private types, and even if that private code should + -- escape into different modules, it can only generate a static error there, not a + -- miscompilation. + -- Note that always using `withExporting` would not always be correct either because it is + -- ignored in non-`module`s and thus mismatches with upstream `module`s may again occur. + let res'? ← observing <| withExporting <| go type + if let .ok res' := res'? then + if res != res' then + throwError "Compilation failed, locally inferred compilation type{indentD res}\n\ + differs from type{indentD res'}\n\ + that would be inferred in other modules. This usually means that a type `def` involved \ + with the mentioned declarations needs to be `@[expose]`d. This is a current compiler \ + limitation for `module`s that may be lifted in the future." + return res where + go type := do + if ← isProp type then + return erasedExpr + let type ← whnfEta type + match type with + | .sort u => return .sort u + | .const .. => visitApp type #[] + | .lam n d b bi => + withLocalDecl n bi d fun x => do + let d ← go d + let b ← go (b.instantiate1 x) + if b.isErased then + return b + else + return Expr.lam n d (b.abstract #[x]) bi + | .forallE .. => visitForall type #[] + | .app .. => type.withApp visitApp + | .fvar .. => visitApp type #[] + | .proj ``Subtype 0 (.const ``IO.RealWorld.nonemptyType []) => + return mkConst ``lcRealWorld + | _ => return mkConst ``lcAny whnfEta (type : Expr) : MetaM Expr := do let type ← whnf type let type' := type.eta @@ -158,12 +180,12 @@ where let d := d.instantiateRev xs withLocalDecl n bi d fun x => do let isBorrowed := isMarkedBorrowed d - let mut d := (← toLCNFType d).abstract xs + let mut d := (← go d).abstract xs if isBorrowed then d := markBorrowed d return .forallE n d (← visitForall b (xs.push x)) bi | _ => - let e ← toLCNFType (e.instantiateRev xs) + let e ← go (e.instantiateRev xs) return e.abstract xs visitApp (f : Expr) (args : Array Expr) := do @@ -178,7 +200,7 @@ where if ← isProp arg <||> isPropFormer arg then result := mkApp result erasedExpr else if ← isTypeFormer arg then - result := mkApp result (← toLCNFType arg) + result := mkApp result (← go arg) else result := mkApp result (mkConst ``lcAny) return result diff --git a/src/Lean/Meta/LazyDiscrTree.lean b/src/Lean/Meta/LazyDiscrTree.lean index 88a49c6c29..5be3a1ab8a 100644 --- a/src/Lean/Meta/LazyDiscrTree.lean +++ b/src/Lean/Meta/LazyDiscrTree.lean @@ -427,7 +427,7 @@ def targetPath (e : Expr) : MetaM (Array Key) := do buildPath op (root := true) (todo.push e) (.mkEmpty initCapacity) /- Monad for finding matches while resolving deferred patterns. -/ -@[reducible] +@[reducible, expose /- for codegen -/] def MatchM α := StateRefT (Array (Trie α)) MetaM def runMatch (d : LazyDiscrTree α) (m : MatchM α β) : MetaM (β × LazyDiscrTree α) := do diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean index dc61904213..d569d223a8 100644 --- a/src/Lean/Meta/Tactic/Grind/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Types.lean @@ -472,6 +472,7 @@ inductive NewFact where | fact (prop proof : Expr) (generation : Nat) -- This type should be considered opaque outside this module. +@[expose] -- for codegen def ENodeMap := PHashMap ExprPtr ENode instance : Inhabited ENodeMap where default := private (id {}) -- TODO(sullrich): `id` works around `private` not respecting the expected type diff --git a/src/Std/Sync/Channel.lean b/src/Std/Sync/Channel.lean index bad33f0355..cb9c02edbb 100644 --- a/src/Std/Sync/Channel.lean +++ b/src/Std/Sync/Channel.lean @@ -613,10 +613,10 @@ end Bounded /-- This type represents all flavors of channels that we have available. -/ -private inductive Flavors (α : Type) where - | unbounded (ch : Unbounded α) - | zero (ch : Zero α) - | bounded (ch : Bounded α) +inductive Flavors (α : Type) where + | private unbounded (ch : Unbounded α) + | private zero (ch : Zero α) + | private bounded (ch : Bounded α) deriving Nonempty end CloseableChannel @@ -629,6 +629,7 @@ Additionally `Std.CloseableChannel` can be closed if necessary, unlike `Std.Chan This introduces a need for error handling in some cases, thus it is usually easier to use `Std.Channel` if applicable. -/ +@[expose] -- for codegen def CloseableChannel (α : Type) : Type := CloseableChannel.Flavors α /-- @@ -640,6 +641,7 @@ Additionally `Std.CloseableChannel.Sync` can be closed if necessary, unlike `Std This introduces the need to handle errors in some cases, thus it is usually easier to use `Std.Channel` if applicable. -/ +@[expose] -- for codegen def CloseableChannel.Sync (α : Type) : Type := CloseableChannel α instance : Nonempty (CloseableChannel α) := diff --git a/src/Std/Time/Format/Basic.lean b/src/Std/Time/Format/Basic.lean index 731cc37290..2a00043303 100644 --- a/src/Std/Time/Format/Basic.lean +++ b/src/Std/Time/Format/Basic.lean @@ -558,7 +558,7 @@ instance : Coe TimeZone Awareness where coe := .only set_option linter.missingDocs false in -- TODO -@[simp] +@[simp, expose /- for codegen -/] def type (x : Awareness) : Type := match x with | .any => ZonedDateTime @@ -771,6 +771,7 @@ private def toIsoString (offset : Offset) (withMinutes : Bool) (withSeconds : Bo data set_option linter.missingDocs false in -- TODO +@[expose /- for codegen -/] def TypeFormat : Modifier → Type | .G _ => Year.Era | .y _ => Year.Offset @@ -1273,7 +1274,7 @@ private def formatPartWithDate (date : DateTime tz) (part : FormatPart) : String | .string s => s set_option linter.missingDocs false in -- TODO -@[simp] +@[simp, expose /- for codegen -/] def FormatType (result : Type) : FormatString → Type | .modifier entry :: xs => (TypeFormat entry) → (FormatType result xs) | .string _ :: xs => (FormatType result xs) diff --git a/src/lake/Lake/Build/Key.lean b/src/lake/Lake/Build/Key.lean index 95bb966516..7b3ffc3b78 100644 --- a/src/lake/Lake/Build/Key.lean +++ b/src/lake/Lake/Build/Key.lean @@ -33,6 +33,7 @@ A build key with some missing info. * Module package targets are supported via a fake `packageTarget` with a target name ending in `moduleTargetIndicator`. -/ +@[expose] -- for codegen public def PartialBuildKey := BuildKey namespace PartialBuildKey diff --git a/src/lake/Lake/Util/Cli.lean b/src/lake/Lake/Util/Cli.lean index 94c06afcb5..8da700d987 100644 --- a/src/lake/Lake/Util/Cli.lean +++ b/src/lake/Lake/Util/Cli.lean @@ -18,6 +18,7 @@ Defines the abstract CLI interface for Lake. /-! # Types -/ +@[expose] -- for codegen public def ArgList := List String @[inline] public def ArgList.mk (args : List String) : ArgList := diff --git a/tests/lean/run/grind_bintree.lean b/tests/lean/run/grind_bintree.lean index 8d192a8cb3..7aeb71589c 100644 --- a/tests/lean/run/grind_bintree.lean +++ b/tests/lean/run/grind_bintree.lean @@ -1,6 +1,6 @@ module reset_grind_attrs% -public section -- TODO: workaround for private declaration + dot-notation issue + attribute [grind] List.append_assoc List.cons_append List.nil_append inductive Tree (β : Type v) where diff --git a/tests/lean/run/grind_ite.lean b/tests/lean/run/grind_ite.lean index 906949f91c..2f022bf4c2 100644 --- a/tests/lean/run/grind_ite.lean +++ b/tests/lean/run/grind_ite.lean @@ -1,7 +1,7 @@ module public import Std.Data.HashMap public import Std.Data.TreeMap -public section -- TODO: Workaround for private declaration + dot-notation issue + /-! # If normalization diff --git a/tests/pkg/module/Module/Basic.lean b/tests/pkg/module/Module/Basic.lean index 49f675601f..e6a0ff0a25 100644 --- a/tests/pkg/module/Module/Basic.lean +++ b/tests/pkg/module/Module/Basic.lean @@ -36,6 +36,21 @@ info: @[reducible, expose] def fabbrev : Nat := #guard_msgs in #print fabbrev +/-- A non-exposed function type. -/ +public def Fun := Nat → Nat + +/-! The compiler should check it has sufficient information about types available. -/ + +/-- +error: Compilation failed, locally inferred compilation type + (Nat → Nat) → Nat → Nat +differs from type + (Nat → Nat) → lcAny +that would be inferred in other modules. This usually means that a type `def` involved with the mentioned declarations needs to be `@[expose]`d. This is a current compiler limitation for `module`s that may be lifted in the future. +-/ +#guard_msgs in +public def Fun.mk (f : Nat → Nat) : Fun := f + #guard_msgs(drop warning) in /-- A theorem. -/ public theorem t : f = 1 := testSorry