Add example to docs/language/informal/super-bounded-types.md.

This CL adds an example to super-bounded-types.md in order to motivate
the definition of what it means for a parameterized type based on a
type alias to be super-bounded. The definition says that we must check
the actual type arguments relative to the formal type parameter
list of the given `typedef` as well as the right hand side, replacing
the formals by the given actual type arguments. The example shows that
the right hand side can be ill-bounded even though the check that we
apply based on the formal type parameter bounds (that is, the check
that we apply to class types) succeeds.

A rendered version of super-bounded-types.md corresponding to patchset
6 is available here:
https://gist.github.com/eernstg/fc12eeb23064a2578a936b443461dde4.

Change-Id: I33dc6ced592f53160bc6f933558bfface46cd329
Reviewed-on: https://dart-review.googlesource.com/56668
Commit-Queue: Erik Ernst <eernst@google.com>
Reviewed-by: Leaf Petersen <leafp@google.com>

docs/language/informal/super-bounded-types.md

@@ -2,7 +2,7 @@
 
 **Author**: eernst@.
 
-**Version**: 0.5 (2018-01-11).
+**Version**: 0.6 (2018-05-25).
 
 **Status**: Under implementation.
 
@@ -348,6 +348,51 @@ super-bounded. Similarly, `G<Object>` is a super-bounded type because
 `void Function(A<Object>)` is well-bounded because `A<Object>` is
 super-bounded.*
 
+*Note that it is necessary to require that the right hand side of a type
+alias declaration is taken into account when determining that a given
+application of a type alias to an actual type argument list is correctly
+super-bounded. That is, we do not think that it is possible for a
+(reasonable) constraint specification mechanism on the formal type
+parameters of a type alias declaration to ensure that all arguments
+satisfying those constraints will also be suitable for the type on the
+right hand side. In particular, we may use simple upper bounds and
+F-bounded constraints (as we have always done), perform and pass the
+'correctly super-bounded' check on a given parameterized type based on a
+type alias, and still have a right hand side which is not well-bounded:*
+```dart
+class B<X extends List<num>> {}
+typedef H<Y extends num> = void Function(B<List<Y>>);
+typedef K<Y extends num> = B<List<Y>> Function(B<List<Y>>);
+
+H<Object> myH = null; // Error!
+```
+*`H<Object>` is a compile-time error because it is not regular-bounded
+(`Object <: num` does not hold), and it is also not correctly
+super-bounded: `Null` does satisfy the constraint in the declaration of
+`Y`, but `H<Object>` gives rise to the right hand side
+`void Function(B<List<Object>>)`, and that is not a well-bounded type:
+It is not regular-bounded (`List<Object> <: List<num>` does not hold),
+and it does not become a regular-bounded type by the type replacements
+(that yield `void Function(B<List<Object>>)` because that occurrence of
+`Object` is contravariant).*
+
+*Semantically, this failure may be motivated by the fact that `H<Object>`,
+were it allowed, would not be a supertype of `H<T>` for all the `T` where
+`H<T>` is regular-bounded. So it would not be capable of playing the role
+as a "default type" that abstracts over all the possible actual types that
+are expressible using `H`. For example, a variable declared like
+`List<H<Object>> x;` would not be allowed to hold a value of type
+`List<H<num>>` because the latter is not a subtype of the former.*
+
+*In the given situation it is possible to express such a default type:
+`H<Null>` is actually a common supertype of `H<T>` for all `T` such that
+`H<T>` is regular-bounded. However, `K` shows that this is not always the
+case: There is no type `S` such that `K<S>` is a common supertype of `K<T>`
+for all those `T` where `K<T>` is regular-bounded. Facing this situation,
+we prefer to bail out rather than implicitly allow some kind of
+super-bounded type (assuming that we amend the rules such that it is not an
+error) which would not abstract over all possible instantiations anyway.*
+
 *The subtype relations for super-bounded types follow directly from the
 extension of generic covariance to include actual type arguments that
 violate the declared bounds. For the example in the Motivation section, `D`
@@ -535,6 +580,9 @@ class types like `C<C<dynamic>>` that we have already argued are useful.
 
 ## Updates
 
+*   Version 0.6 (2018-05-25), added example showing why we must check the
+    right hand side of type aliases.
+
 *   Version 0.5 (2018-01-11), generalized to allow replacement of top types
     covariantly and bottom types contravariantly. Introduced checks on
     parameterized type aliases (such that bounds declared for the type