Union refinement permits narrowing branches of tag union pattern matches to the subset of variants not covered by previous branches. For example,

t : [User, Admin, SuperAdmin]
when t is
  User -> ... 
  other -> ... # here, other has type [Admin, SuperAdmin]

This kind of behavior is also known as “type narrowing” and “flow-sensitive typing” in other languages, like TypeScript. The behavior would provide for a subtyping look-and-feel to Roc, where it’s not otherwise. Many Roc users have run into a want for this kind of behavior.

This document describes one approach for type refinement in Roc specific to only refining tag unions in when expressions. Control-flow-sensitive typing in general is not considered. The approach is intended to be “zero-cost” in that it is sugar for what would otherwise be an identical transformation made by a user.

Summary

• Tag unions may be refined if they bound to named variables in when branch patterns, like in the introductory example.

• A named variable pattern like

  when t is
    User -> ...
    other -> ...
  

  types other as the type of t without all of the exhaustively-matches types proceeding the type of other - in this case, other is typed as typeof t - typeof User. The behavior of - operator is described explicitly below, but can be thought of removing the appropriate set of tags from a tag union type.

• An as-pattern pattern like

  t : [A U8, B Str, C]
  when t is
    A _ | B _ as x -> ...
    C -> ...
  

  types x as explicitly the type of A _ | B _, which is the union type [A U8, B Str].

• No other patterns or variables can undergo union refinement. Condition variables, variables in if expressions, etc. are not refined.

• Union refinements effect only non-recursive tag unions, and the first level of recursive tag unions.

• Union refinements never descend under recursive types’ recursion points. (See this example)

• Union refinements compile down to the equivalent manual transformation that would have to be done by hand, except that the compiler ensures type-safety and can elide crash branches where they otherwise would be necessary.

• If union refinements do not change the type, the compiler elides the transformation.

• If union refinements change the type but not the runtime value of a tag union, the compiler may in the future elide the transformation. This is an optimization that could be applied to many other types (”transmutation”) as well.

Inference Scheme

As a quick primer, the inference scheme for pattern matches

when condition is
  pattern_1 -> ...
  pattern_2 -> ...

consists of determining typeof(patterns) and typeof(condition) independently, and then checking that those types are equivalent (making them equal under unification). For example,

t : [User, Admin, SuperAdmin]
when t is
  User -> ... 
  other -> ...

# typeof(condition) = typeof t = [User, Admin, SuperAdmin]
# typeof(patterns)  = typeof User ~ typeof other = [User] ~ * = [User]
# => typeof(t) = [User, Admin, SuperAdmin] ~ [User] = [User, Admin, SuperAdmin]