Skip to content

Clarification may be useful in flow-analysis.md #4506

@eernstg

Description

@eernstg

The flow-analysis definition of toi_promote has the following:

  • toi_promote(declared, promotionChain, tested, written), where ...
    ...
    • If the written type is in p2, and written <: provisionalType, then
      newPromotionChain is [...promotionChain, written]. ...
    • Otherwise (when written is not in p2):

This is somewhat confusing to read because it seems to skip over the case where written is in p2, but written <: provisionalType does not hold.

However, written <: provisionalType is guaranteed to hold in all cases because of the preconditions which are specified in order to use toi_promote (and because the only "call site" for toi_promote is known to satisfy those preconditions).

Granted, this is a request for a tiny change, but I do think the rule will be easier to read if "and written <: provisionalType" is removed, or it is changed to commentary.

Metadata

Metadata

Assignees

No one assigned

    Labels

    flow-analysisDiscussions about possible future improvements to flow analysisspecification

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions