fix: lake: meta import transitivity (#11683)

This PR fixes an inconsistency in the way Lake and Lean view the
transitivity of a `meta import`. Lake now works as Lean expects and
includes the meta segment of all transitive imports of a `meta import`
in its transitive trace.

src/lake/Lake/Build/Module.lean

@@ -327,13 +327,13 @@ private def ModuleImportInfo.addImport
           |>.mix expInfo.artsTrace.withoutInputs
           |>.withoutInputs
       }
+  let info := {info with
+    metaTransTrace := info.metaTransTrace
+      |>.mix expInfo.metaTransTrace
+      |>.mix expInfo.metaArtsTrace.withoutInputs
+      |>.withoutInputs
+  }
   if imp.isExported then
-    let info := {info with
-      metaTransTrace := info.metaTransTrace
-        |>.mix expInfo.metaTransTrace
-        |>.mix expInfo.metaArtsTrace.withoutInputs
-        |>.withoutInputs
-    }
     if imp.isMeta then
       {info with
         transTrace := info.transTrace

tests/lake/tests/module/Test/Module/MetaImportImport.lean

@@ -0,0 +1,3 @@
+module
+
+meta import Test.Module.Import

tests/lake/tests/module/test.sh

@@ -141,8 +141,10 @@ test_run build Test.Module.Import Test.Module.PublicImport --no-build
 # should trigger a rebuild on a direct `meta import`
 test_out "Built Test.Module.MetaImport" build Test.Module.MetaImport -v
 test_out "Built Test.Module.PublicMetaImport" build Test.Module.PublicMetaImport -v
-# should trigger a rebuild on a transitive `meta import`
+# should trigger a rebuild on a `meta import` of a transitive `public import`
 test_out "Built Test.Module.MetaImportPublicImport" build Test.Module.MetaImportPublicImport -v
+# should trigger a rebuild on a `meta import` of a transitive private `import`
+test_out "Built Test.Module.MetaImportImport" build Test.Module.MetaImportImport -v
 # should trigger a rebuild on module transitive import of a `public meta import`
 test_out "Built Test.Module.ImportPublicMetaImport" build Test.Module.ImportPublicMetaImport -v
 # should not trigger a rebuild on module transitive import of a private `meta import`