Additional documentation on type refinement?

[cpitclaudel]

A few months back I started writing missing docs for type refinement. As part of the process of writing that doc a few soundness bugs were found, and I focused on fixing them instead, so the following text was never used:

 docs/DafnyRef/Refinement.md | 70 +++++++++++++++++++++++++++++++++++--
 1 file changed, 68 insertions(+), 2 deletions(-)

diff --git a/docs/DafnyRef/Refinement.md b/docs/DafnyRef/Refinement.md
index b30dbc48f..ad8508b89 100644
--- a/docs/DafnyRef/Refinement.md
+++ b/docs/DafnyRef/Refinement.md
@@ -300,7 +300,73 @@ TODO
 TODO
 
 ## 21.10. Type declarations
--- opaque, type synonym, subset, newtype, datatype
 
-TODO
+Types can be refined in two ways:
+
+- Turning an opaque type into a concrete type;
+- Adding members to a datatype or a newtype.
+
+For example, consider the following abstract module:
+
+```dafny
+abstract module Parent {
+  type T
+  type B = bool
+  type S = s: string | |s| > 0 witness "!"
+  newtype Pos = n: nat | n > 0 witness 1
+  datatype Bool = True | False
+}
+```
+
+In this module, type `t` is opaque and hence can be refined with any type,
+including class types.  Types `B`, `S`, `Pos`, and `Bool` are concrete and
+cannot be refined further, except (for `Pos` and `Bool`) by giving them
+additional members or attributes (or refining their existing members, if any).
+Hence, the following are valid refinements:
+
+```dafny
+module ChildWithTrait refines Parent {
+  trait T {}
+}
+
+module ChildWithClass refines Parent {
+  class T {}
+}
+
+module ChildWithSynonymType refines Parent {
+  type T = bool
+}
+
+module ChildWithSubsetType refines Parent {
+  type T = s: seq<int> | s != [] witness [0]
+}
+
+module ChildWithDataType refines Parent {
+  datatype T = True | False
+}
+
+abstract module ChildWithExtraMembers refines Parent {
+  newtype Pos ... {
+    method Print() { print this; }
+  }
+
+  datatype Bool ... {
+    function method AsDafnyBool() : bool { this.True? }
+  }
+}
+```
+
+(The last example is marked `abstract` because it leaves `t` opaque.)
+
+Note that datatype constructors, codatatype destructors, and newtype definitions
+cannot be refined: it is not possible to add or remove constructors to a
+`datatype`, nor to change destructors to a `codatatype`, nor to change the base
+type, constraint, or witness of a `newtype`.
+
+When a type takes arguments, its refinement must use the same type arguments
+with the same type constraints and the same variance.
 
+When a type has type constraints, these type constraints must be preserved by
+refinement.  This means that a type declaration `type T(!new)` cannot be refined
+by a `class T`, for example. Similarly, a `type T(00)` cannot be refined by a
+subset type with a `witness *` clause.

We now have some documentation for this section, so instead of making a PR I'm just posting the text here. @davidcok , could you see whether there's anything worth merging into the docs that we now have.

[davidcok]

OK - I'll take on this task at some point -- integrating it into the current text as needed.