Subsetting type conformance is not checked, although redefinition type conformance is

[mhoh79]

Subsetting type conformance is not checked, although redefinition type conformance is

Version: v0.3.0, sysml-grpc-linux-amd64, SHA-256 b39b720e020c325020af95c33640ad3583c938d74c40d29a0741fab6c03412de
Path: ParseFile + Resolve over gRPC, one inline document

Summary

The service validates that a redefining feature's type conforms to what it redefines, and it validates the multiplicity bound for subsetting and redefinition alike — but it does not validate that a subsetting feature's type conforms to what it subsets. That case produces no error, no warning, and no diagnostic of any kind.

The asymmetry looks unintentional rather than deliberate: the multiplicity rule is already applied to both relations (its message says so — "Subsetting/redefining feature should not have larger multiplicity upper bound"), and the redefinition type check already computes and formats exactly the diagnostic the subsetting case needs.

Reproduction

Each block is one document through ParseFile, then Resolve. Diagnostics are the union of both, de-duplicated.

1. Subsetting with a non-conforming type — expected a diagnostic, got none

package P {
	class A;
	class B;
	feature g : A;
	feature f : B subsets g;
}

→ (no diagnostics at all)

f subsets g asserts that f's values are among g's. g holds As and f is a B, which is unrelated to A, so no value of f can be a value of g.

2. Control — subsetting with a conforming type

package P {
	class A;
	class B specializes A;
	feature g : A;
	feature f : B subsets g;
}

→ (no diagnostics at all)

Correct, and together with (1) it shows the check is absent rather than merely lenient: the well-formed and the ill-formed model are indistinguishable in the output.

3. The same violation through redefinition — reported

package P {
	class A;
	class B;
	class C { feature g : A; }
	class D specializes C { feature g : B redefines C::g; }
}

→ [error] g (typed by B) redefines g (typed by A): types do not conform

4. The multiplicity half of subsetting — reported

package P {
	class A;
	feature g : A [0..5];
	feature f : A subsets g [0..10];
}

→ [warning] Subsetting/redefining feature should not have larger multiplicity upper bound

5. Control — the resolver is working

package P {
	class A;
	feature g : Nonexistent;
}

→ [error] unresolved reference: Nonexistent

Also reproduces in SysML usage syntax

Same silence with part def / part in a .sysml document, so it is not specific to the KerML surface:

package P {
	part def A;
	part def B;
	part g : A;
	part f : B subsets g;
}

→ (no diagnostics at all), and likewise with part def B :> A for the conforming control.

Expected

Case (1) reports a diagnostic in the shape case (3) already produces — e.g. f (typed by B) subsets g (typed by A): types do not conform.

Why it matters to a downstream consumer

Silence is indistinguishable from a clean bill of health. A tool that asks the service to validate a model gets an empty diagnostic list and has no way to learn that half of the subsetting check did not run — so it reports the model as sound. For consumers that build a specialization/subsetting graph out of the parsed model (we translate one to OWL), an unchecked subsetting edge propagates into everything derived from it.

Environment

Reproduced on Linux x86-64 against the published v0.3.0 release asset, checksum as above, over the gRPC API only. Happy to supply the exact request payloads if useful.

[HuiJun]

We really have to fix our integration permissions. However, here is our reply to your issue:

Thanks for the careful report — the four models reproduce exactly as described on current main too. After checking the KerML 1.0 specification text, though, we believe the silence on the subsetting case is correct and the asymmetry with redefinition is intentional. Recording the reasoning here:

Subsetting adds types; it does not require the declared type to conform.

• KerML 1.0 §8.3.3.3.4 (Feature::type): "The types of a Feature are derived from its typings and the types of its subsettings." So in feature f : B subsets g; with feature g : A;, f is typed by both A and B — its values are instances of the intersection.
• §8.3.3.3.10 (Subsetting): "the co-domain (intersection of the types) of the subsettingFeature must specialize the co-domain of the subsettedFeature" — which holds by construction given the derivation above. The normative constraints on Subsetting are only validateSubsettingConstantConformance, validateSubsettingFeaturingTypes and validateSubsettingUniquenessConformance (plus the multiplicity warning); there is no type-conformance constraint.
• §7.3.4.4: "a subsetting feature can constrain its featured types to be specializations of those of the subsetted feature and add additional feature types."

The OMG training corpus relies on this shape — Model Library Example.sysml declares abstract occurrence causes : Cause[*] nonunique :> situations; where situations : Situation[*] and Cause does not specialize Situation — so a diagnostic here would reject the reference's own library model. The pinned pilot implementation is also silent on model (1), consistent with the spec.

Why redefinition is different. A redefinition replaces the redefined feature in the specializing type rather than narrowing it. §8.3.3.3.8 does not declare a type-conformance constraint either — redefinition-type-mismatch is an OpenSysML extension, which is why the pilot is silent on your model (3) while we report it.

For downstream consumers (e.g. an OWL export): the sound reading of f subsets g with unrelated declared types is that f's type is A ⊓ B, not that the edge is invalid. If A and B are meant to be disjoint, KerML expresses that with disjoint from, and a subsetting between features whose types are declared disjoint would be a genuinely empty (though still well-formed) feature.

We're documenting this adjudication in the compliance record (docs/project/spec-compliance.md, Redefinition in a Specialization) with the clause citations above so it is discoverable. If you read the clauses differently, or have a model where the intersection reading gives a wrong result, we'd be glad to revisit.