Compute the type T implied for a value v matched by a pattern pat (with expected type pt).
Compute the type T implied for a value v matched by a pattern pat (with expected type pt).
Usually, this is the pattern's type because pattern matching implies instance-of checks.
However, Stable Identifier and Literal patterns are matched using ==,
which does not imply a type for the binder that binds the matched value.
See SI-1503, SI-5024: don't cast binders to types we're not sure they have
TODO: update spec as follows (deviation between **):
A pattern binder x@p consists of a pattern variable x and a pattern p. The type of the variable x is the static type T **IMPLIED BY** the pattern p. This pattern matches any value v matched by the pattern p **Deleted: , provided the run-time type of v is also an instance of T, ** and it binds the variable name to that value.
Addition:
A pattern p _implies_ a type T if the pattern matches only values of the type T.