From ada6b9ee9baf601c7d4e217ad571f5f1e57525fc Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Wed, 31 May 2023 12:38:48 +0200
Subject: [PATCH] Clarified tear-offs of methods with covariant parameters

---
 specification/dartLangSpec.tex | 32 ++++++++++++++++++++++++--------
 1 file changed, 24 insertions(+), 8 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index eb1f8467f1..4ba52a49e3 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -15244,7 +15244,11 @@ \subsubsection{Instance Method Closurization}
 \LMHash{}%
 For each parameter $p_j$, $j \in 1 .. n+k$, if $p_j$ is covariant
 (\ref{covariantParameters})
-then $T_j$ is \DYNAMIC. %% No user code will see this, avoid downcast in body.
+then $T_j$ is \code{Object?}.
+The corresponding actual argument in the body is replaced by
+\code{$p_j$\,\,\AS\,\,$T'_j$}
+where $T'_j$ is the type which would be $T_j$ if $p_j$ had not been covariant
+(\commentary{that is, it is computed as specified below}).
 
 \commentary{%
 This is concerned with the dynamic type of the function object obtained by
@@ -15257,12 +15261,15 @@ \subsubsection{Instance Method Closurization}
 }
 
 \LMHash{}%
-Otherwise, if $T$ is a non-generic class then for $j \in 1 .. n+k$,
+Otherwise
+(\commentary{when $p_j$ is not covariant}),
+if $T$ is a non-generic class then for $j \in 1 .. n+k$,
 $T_j$ is a type annotation that denotes the same type
 (\ref{typeType})
 as that which is denoted by the type annotation on
 the corresponding parameter declaration in $D$.
-If that parameter declaration has no type annotation then $T_j$ is \DYNAMIC.
+If that parameter declaration has no type annotation
+then $T_j$ is \code{Object?}.
 
 \LMHash{}%
 Otherwise $T$ is a generic instantiation of a generic class $G$.
@@ -15271,7 +15278,8 @@ \subsubsection{Instance Method Closurization}
 Then $T_j$ is a type annotation that denotes
 $[t''_1/X''_1, \ldots, t''_{s''}/X''_{s''}]S_j$,
 where $S_j$ is the type annotation of the corresponding parameter in $D$.
-If that parameter declaration has no type annotation then $T_j$ is \DYNAMIC.
+If that parameter declaration has no type annotation
+then $T_j$ is \code{Object?}.
 
 \LMHash{}%
 There is one way in which
@@ -15400,7 +15408,11 @@ \subsubsection{Super Closurization}
 \LMHash{}%
 For each parameter $p_j$, $j \in 1 .. n+k$, if $p_j$ is covariant
 (\ref{covariantParameters})
-then $T_j$ is \DYNAMIC.
+then $T_j$ is \code{Object?}.
+The corresponding actual argument in the body is replaced by
+\code{$p_j$\,\,\AS\,\,$T'_j$}
+where $T'_j$ is the type which would be $T_j$ if $p_j$ had not been covariant
+(\commentary{that is, it is computed as specified below}).
 
 \commentary{%
 This is concerned with the dynamic type of the function object obtained by
@@ -15413,12 +15425,15 @@ \subsubsection{Super Closurization}
 }
 
 \LMHash{}%
-Otherwise, if $S$ is a non-generic class then for $j \in 1 .. n+k$,
+Otherwise
+(\commentary{when $p_j$ is not covariant}),
+if $S$ is a non-generic class then for $j \in 1 .. n+k$,
 $T_j$ is a type annotation that denotes the same type
 (\ref{typeType})
 as that which is denoted by the type annotation on
 the corresponding parameter declaration in $D$.
-If that parameter declaration has no type annotation then $T_j$ is \DYNAMIC.
+If that parameter declaration has no type annotation
+then $T_j$ is \code{Object?}.
 
 \LMHash{}%
 Otherwise $S$ is a generic instantiation of a generic class $G$.
@@ -15427,7 +15442,8 @@ \subsubsection{Super Closurization}
 Then $T_j$ is a type annotation that denotes
 $[t''_1/X''_1, \ldots, t''_{s''}/X''_{s''}]S_j$,
 where $S_j$ is the type annotation of the corresponding parameter in $D$.
-If that parameter declaration has no type annotation then $T_j$ is \DYNAMIC.
+If that parameter declaration has no type annotation
+then $T_j$ is \code{Object?}.
 
 \LMHash{}%
 There is one way in which