[improve documentation for core type system
John Meacham <john@repetae.net>**20080221042003] hunk ./E/TypeCheck.hs 41
-    PTS type checker
-    core is the following PTS
-    S = (*,!,**,#,(#),##)
-    A = (*::**,#::##,(#)::##,!::**)
+Jhc's core is based on a pure type system. A pure type system (also called a
+PTS) is actually a parameterized set of type systems. Jhc's version is
+described by the following.
hunk ./E/TypeCheck.hs 45
+    Sorts  = (*,!,**,#,(#),##)
+    Axioms = (*::**,#::##,(#)::##,!::**)
hunk ./E/TypeCheck.hs 48
-    * is the sort of boxed values
-    ! is the sort of boxed strict values
-    ** is the supersort of all boxed value
-    # is the sort of unboxed values
+
+    *   is the sort of boxed values
+    !   is the sort of boxed strict values
+    **  is the supersort of all boxed value
+    #   is the sort of unboxed values
hunk ./E/TypeCheck.hs 54
-    ## is the supersort of all unboxed values
-    we also have user defined kinds, which are always of supersort ##
+    ##  is the supersort of all unboxed values
hunk ./E/TypeCheck.hs 56
-    notice that functions are always boxed, but may be strict if they take an unboxed tuple as an argument
+    in addition there exist user defined kinds, which are always of supersort ##
hunk ./E/TypeCheck.hs 58
-     -- these rules apply to lambda abstractions, data constructors can be _defined_ to have types that would be invalid otherwise
-    as a shortcut we will use *# to mean either * or # and so forth
hunk ./E/TypeCheck.hs 59
+The following Rules table shows what sort of abstractions are allowed, a rule
+of the form (A,B,C) means you can have functions of things of sort A to things
+of sort B and the result is something of sort C. _Function_ in this context
+subsumes both term and type level abstractions. Notice that functions are
+always boxed, but may be strict if they take an unboxed tuple as an argument.
+(TODO: explain strict in this context) These type system rules apply to lambda
+abstractions. it is possible to inherit values from the environment that would
+not be typable via lambda abstractions. for instance, although a data
+constructor may have a functional type, it was not created via a lambda
+abstraction so these rules do not apply.
+
+    as a shortcut we will use *# to mean either * or # and so forth
hunk ./E/TypeCheck.hs 73
-    R =
+    Rules =
hunk ./E/TypeCheck.hs 84
+    The defining feature of boxed values is
+
hunk ./E/TypeCheck.hs 88
-    this PTS is functional but not injective
+    This PTS is functional but not injective
+