liberal-type-synonyms.md

@@ -6,7 +6,8 @@
 See the [ GHC Documentation](http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html#type-synonyms) on this extension.
 
 
-The basic idea is that type validity checking is done *after expanding type synonyms*.  This means that type synonyms can be written unsaturated, as long as the result of expanding synonyms leaves everything saturated.  This is sometimes quite useful.
+The basic idea is that type validity checking is done *after expanding type synonyms*. 
+This means, for example, that type synonyms can be written unsaturated, as long as the result of expanding synonyms leaves everything saturated.  This is sometimes quite useful.
 
 
 There are also interactions with [RankNTypes](rank-n-types) - a type synonym may expand to a quantified type.
@@ -14,12 +15,19 @@ There are also interactions with [RankNTypes](rank-n-types) - a type synonym may
 ## Proposal
 
 
-Adopt GHC's approach to type synonym expansion.
+Adopt GHC's approach to type synonym expansion. Specifically, these conditions are checked only *after* expansion:
 
-## Design choices
+- No partial applications of type synonyms
+- No 'forall' types as an argument to a type constructor
+- An instance head is of form `C (T ...)`, where `T` is a *data* type.
 
 
-Should kind inference be done before, or after expanding type synonyms?  That is, should a type synonym have a fixed kind or not?
+However these conditions may be broken *before* expansion of type synonyms.
+
+## Kind checking
+
+
+Should kind checking be done before, or after expanding type synonyms?  That is, should a type synonym have a fixed kind or not?
 
 
 Currently GHC does kind inference before expanding type synonyms, and gives each type synonym a fixed kind.  The following program is rejected: