§3.3.(d) Typing rules

A parameter mapping (implicit by parameter position or explicit by a with clause) is well typed if the left hand side conforms to the right hand side, either by

A result mapping (implicit or explicit by a with clause) is well typed, if the value at the right hand side conforms to the left hand side according to the rules given above, except that translation polymorphism here applies lifting instead of lowering.