From 9e48cc7f25644505f4b4e6530e682d487f0f956b Mon Sep 17 00:00:00 2001 From: Erik Ernst Date: Thu, 20 Dec 2018 13:33:30 +0000 Subject: [PATCH] Adjust specification of type tests to include promotion to X & S Addresses https://github.com/dart-lang/sdk/issues/35314. Change-Id: I97550187255c5ac896bfea881de85c5e97e9930e Reviewed-on: https://dart-review.googlesource.com/c/85921 Reviewed-by: Lasse R.H. Nielsen --- docs/language/dartLangSpec.tex | 24 ++++++++++++++++-------- 1 file changed, 16 insertions(+), 8 deletions(-) diff --git a/docs/language/dartLangSpec.tex b/docs/language/dartLangSpec.tex index 43e099266c6..53226764053 100644 --- a/docs/language/dartLangSpec.tex +++ b/docs/language/dartLangSpec.tex @@ -10457,13 +10457,19 @@ Users should test for the null object (\ref{null}) directly rather than via type \LMHash{}% The is-expression \code{$e$ \IS{}! $T$} is equivalent to \code{!($e$ \IS{} $T$)}. -% Add flow dependent types - \LMHash{}% Let $v$ be a local variable (\commentary{which can be a formal parameter}). -%% TODO(eernst): Cf. issue https://github.com/dart-lang/sdk/issues/35314. -An is-expression of the form \code{$v$ \IS{} $T$} shows that $v$ has type $T$ -if{}f $T$ is a subtype of the type $S$ of the expression $v$. +An is-expression of the form \code{$v$ \IS{} $T$} +shows that $v$ has type $T$ +if $T$ is a subtype of the type of the expression $v$. +% +Otherwise, +if the declared type of $v$ is the type variable $X$, +and $T$ is a subtype of the bound of $X$, +and $X \& T$ is a subtype of the type of the expression $v$, +then $e$ shows that $v$ has type $X \& T$. +% +Otherwise $e$ does not show that $v$ has type $T$ for any $T$. \rationale{ The motivation for the ``shows that v has type T" relation is to reduce spurious errors thereby enabling a more natural coding style. @@ -10474,10 +10480,12 @@ The rule only applies to locals and parameters, as instance and static variables It is pointless to deduce a weaker type than what is already known. Furthermore, this would lead to a situation where multiple types are associated with a variable at a given point, which complicates the specification. -Hence the requirement that \SubtypeNE{T}{S}. +Hence the requirement that the promoted type is a subtype of the current type. -We do not want to refine the type of a variable of type \DYNAMIC{}, as this could lead to more errors rather than fewer. -The opposite requirement, that $T \ne \DYNAMIC{}$ is a safeguard lest $S$ ever be $\bot$. +In any case, it is not an error when a type test does not show +that a given variable does not have a ``better'' type than previously known, +but tools may choose to give a hint in such cases, +if suitable heuristics indicate that a promotion is likely to be intended. } \LMHash{}%