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.

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. -/

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...<s.internalRepresentation.stop)

src/Init/System/Promise.lean

@@ -16,10 +16,6 @@ namespace IO
 
 private opaque PromisePointed : NonemptyType.{0}
 
-private structure PromiseImpl (α : Type) : Type where
-  prom : PromisePointed.type
-  h    : Nonempty α
-
 /--
 `Promise α` allows you to create a `Task α` whose value is provided later by calling `resolve`.
 
@@ -33,7 +29,9 @@ Typical usage is as follows:
 If the promise is dropped without ever being resolved, `promise.result?.get` will return `none`.
 See `Promise.result!/resultD` for other ways to handle this case.
 -/
-def Promise (α : Type) : Type := PromiseImpl α
+structure Promise (α : Type) : Type where
+  private prom : PromisePointed.type
+  private h    : Nonempty α
 
 instance [s : Nonempty α] : Nonempty (Promise α) :=
   by exact Nonempty.intro { prom := Classical.choice PromisePointed.property, h := s }

src/Lean/Compiler/LCNF/Types.lean

@@ -123,27 +123,49 @@ open Meta in
 Convert a Lean type into a LCNF type used by the code generator.
 -/
 partial def toLCNFType (type : Expr) : MetaM Expr := 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 ← 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

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

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

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 α) :=

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)

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

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 :=

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

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
 

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