Fix fatal errors caused by condition on message type field

Ref. eng/recordflux/RecordFlux#1438

CHANGELOG.md

@@ -15,6 +15,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Fixed
 
 - User defined `GNATCOLL_ICONV_OPT` environment variable is ignored (AdaCore/RecordFlux#1289, eng/recordflux/RecordFlux#1437)
+- Fix fatal errors caused by condition on message type field (AdaCore/RecordFlux#1291, eng/recordflux/RecordFlux#1438)
 
 ### Removed
 

rflx/model/message.py

@@ -2549,7 +2549,12 @@ def merged(
             if not inner_message:
                 return message
 
-            message = self._merge_inner_message(message, *inner_message, message_arguments)
+            message = self._merge_inner_message(
+                message,
+                *inner_message,
+                message_arguments,
+                declarations,
+            )
 
     def _check_message_arguments(
         self,
@@ -2604,6 +2609,7 @@ def _merge_inner_message(
         field: Field,
         inner_message: Message,
         message_arguments: Mapping[ID, Mapping[ID, expr.Expr]],
+        declarations: Sequence[TopLevelDeclaration],
     ) -> UncheckedMessage:
         inner_message = self._replace_message_attributes(inner_message.prefixed(f"{field.name}_"))
 
@@ -2616,16 +2622,35 @@ def _merge_inner_message(
             else {}
         )
         structure = []
+        message_types = message.types(declarations)
+        message_dependencies = _dependencies(message_types)
+        message_unqualified_enum_literals = mty.unqualified_enum_literals(
+            message_dependencies,
+            message.package,
+        )
+        message_qualified_enum_literals = mty.qualified_enum_literals(message_dependencies)
+        message_qualified_type_names = mty.qualified_type_names(message_dependencies)
         inner_message_types = inner_message.types
-        dependencies = _dependencies(inner_message_types)
-        inner_message_qualified_enum_literals = mty.qualified_enum_literals(dependencies)
-        inner_message_qualified_type_names = mty.qualified_type_names(dependencies)
+        inner_message_dependencies = _dependencies(inner_message_types)
+        inner_message_qualified_enum_literals = mty.qualified_enum_literals(
+            inner_message_dependencies,
+        )
+        inner_message_qualified_type_names = mty.qualified_type_names(inner_message_dependencies)
+
+        def substitute_message_variables(expression: expr.Expr) -> expr.Expr:
+            return substitute_variables(
+                expression,
+                message_unqualified_enum_literals,
+                message_qualified_enum_literals,
+                message_qualified_type_names,
+                message.package,
+            )
 
         def typed_variable(expression: expr.Expr) -> expr.Expr:
             return typed_expression(
                 expression,
-                inner_message_types,
-                inner_message_qualified_enum_literals,
+                {**message_types, **inner_message_types},
+                {**message_qualified_enum_literals, **inner_message_qualified_enum_literals},
                 inner_message_qualified_type_names,
             )
 
@@ -2655,8 +2680,10 @@ def typed_variable(expression: expr.Expr) -> expr.Expr:
                                 final_link.condition,
                             )
                             .substituted(mapping=substitution)
+                            .substituted(substitute_message_variables)
                             .substituted(typed_variable)
                         )
+                        merged_condition.check_type(rty.Any()).propagate()
                         proof = merged_condition.check(
                             [
                                 *message_constraints(),

tests/unit/model/message_test.py

@@ -3771,7 +3771,7 @@ def test_merge_message_complex() -> None:
 def test_merge_message_recursive() -> None:
     assert_equal(
         deepcopy(M_DBL_REF).merged(
-            [models.integer(), models.enumeration(), msg_no_ref(), msg_smpl_ref()],
+            [OPAQUE, models.integer(), models.enumeration(), msg_no_ref(), msg_smpl_ref()],
         ),
         UncheckedMessage(
             ID("P::Dbl_Ref"),
@@ -4427,6 +4427,120 @@ def test_merge_message_type_message_size_attribute_in_outer_message() -> None:
     assert outer.checked([OPAQUE, inner]) == expected
 
 
+def test_merge_message_with_condition_on_message_type_field() -> None:
+    inner = Message(
+        ID("P::I"),
+        [
+            Link(
+                INITIAL,
+                Field("I"),
+                size=Number(128),
+            ),
+            Link(
+                Field("I"),
+                FINAL,
+            ),
+        ],
+        {
+            Field("I"): OPAQUE,
+        },
+    )
+
+    enumeration = Enumeration(
+        "P::Enumeration",
+        [("E1", Number(1)), ("E2", Number(2)), ("E3", Number(3))],
+        Number(8),
+        always_valid=False,
+    )
+    padding = Integer("P::Padding", Number(0), Number(0), Number(7))
+
+    outer = UncheckedMessage(
+        ID("P::O"),
+        [
+            Link(INITIAL, Field("Flag")),
+            Link(Field("Flag"), Field("Padding")),
+            Link(Field("Padding"), Field("Payload")),
+            Link(
+                Field("Payload"),
+                FINAL,
+                condition=And(
+                    Equal(Variable("Flag"), TRUE),
+                    Equal(Variable("Parameter"), Variable("E1")),
+                ),
+            ),
+        ],
+        [
+            (Field("Parameter"), enumeration.identifier, []),
+        ],
+        [
+            (Field("Flag"), BOOLEAN.identifier, []),
+            (Field("Padding"), padding.identifier, []),
+            (Field("Payload"), inner.identifier, []),
+        ],
+    )
+
+    expected = Message(
+        ID("P::O"),
+        [
+            Link(INITIAL, Field("Flag")),
+            Link(Field("Flag"), Field("Padding")),
+            Link(Field("Padding"), Field("Payload_I"), size=Number(128)),
+            Link(
+                Field("Payload_I"),
+                FINAL,
+                condition=And(
+                    Equal(Variable("Flag"), TRUE),
+                    Equal(Variable("Parameter"), Literal("P::E1")),
+                ),
+            ),
+        ],
+        {
+            Field("Parameter"): enumeration,
+            Field("Flag"): BOOLEAN,
+            Field("Padding"): padding,
+            Field("Payload_I"): OPAQUE,
+        },
+    )
+
+    assert outer.checked([BOOLEAN, OPAQUE, enumeration, padding, inner]) == expected
+
+
+def test_merge_message_with_illegal_condition_on_message_type_field() -> None:
+    inner = Message(
+        ID("P::I"),
+        [
+            Link(INITIAL, Field("I")),
+            Link(Field("I"), FINAL),
+        ],
+        {
+            Field("I"): models.integer(),
+        },
+    )
+
+    outer = UncheckedMessage(
+        ID("P::O"),
+        [
+            Link(INITIAL, Field("O")),
+            Link(Field("O"), FINAL, condition=Equal(TRUE, Number(1, location=Location((1, 2))))),
+        ],
+        [],
+        [
+            (Field("O"), inner.identifier, []),
+        ],
+    )
+
+    with pytest.raises(
+        RecordFluxError,
+        match=(
+            "^"
+            '<stdin>:1:2: model: error: expected enumeration type "__BUILTINS__::Boolean"\n'
+            r"<stdin>:1:2: model: info: found type universal integer \(1\)"
+            "$"
+        ),
+    ):
+        outer.checked([inner])
+
+
 @pytest.mark.skipif(not __debug__, reason="depends on assertion")
 def test_merge_message_with_undeclared_type() -> None:
     with pytest.raises(