more writing

Author: MaximilianAlgehed

docs/Manual.md

@@ -384,51 +384,57 @@ conformsToSpec :: HasSpec a => a -> Specification a -> Bool
 
 ## How we solve the constraints
 
+Before we continue delving into how we use the library and the finer points
+surrounding generics and overloading it's worth-while to take a detour into how
+we solve constraints. Understanding and internalising this will be helpful when
+writing anything but the simplest generators.
+
 The strategy for generating things from `Pred`s is relatively straightforward
 and relies on one key fact: any constraint that has only one free variable `x`
 and where `x` occurs only once can be turned into a `Specification` for `x`.
 
-We say that such constraints _define_ `x` and given a set of constraints `ps`
-and a variable `x` we can split `ps` into the constraints that define `x` and
-any constraints that don't. We can then generate a value from `x` by computing
-a spec for each defining constraint in `ps` and using the `Semigroup` structure
-of `Specification`s to combine them and give them to `genFromSpecT`. Once we obtain a
-value for `x` we can substitute this value in all other constraints and pick
-another variable to solve.
+We say that such constraints _define_ `x` (alt. are _defining_ for `x`) and
+given a set of constraints `ps` and a variable `x` we can split `ps` into the
+constraints that define `x` and any constraints that don't. We can then
+generate a value from `x` by computing a spec for each _defining constraint_ in
+`ps` and using the `Semigroup` structure of `Specification`s to combine them
+and give them to `genFromSpecT`. Once we obtain a value for `x` we can
+substitute this value in all other constraints and pick another variable to
+solve.
 
 For example, given the following constraints on integers `x` and `y`
 
 ```
-  x <. 10
-  3 <=. x
-  y <. x
+x <. 10
+3 <=. x
+y <. x
 ```
 
 we see that `x <. 10` and `3 <=. x.` are defining constraints for `x` and there
-are no defining constraints for `y`. We compute a `Specification` for `x` for each
+are no defining constraints for `y` (yet!). We compute a `Specification` for `x` for each
 constraint, in this case `x <. 10` turns into something like `(-∞,10)` and
 `3 <=. x` turns into `[3, ∞)`. We combine the specs to form `[3, 10)` from which we
 can generate a value, e.g. 4 (chosen by fair dice roll). We then substitute
 `[x := 4]` in the remaining constraints and obtain `y <. 4`, giving us a defining
-constraint for `y`.
+constraint for `y`. We then repeat the process for `y`, giving us a specification
+like `(-∞,4)` for `y`, from which we can generate a value.
 
 ### How to pick the variable order
 
 At this point it should be relatively clear that the order we pick for the
 variables matters a great deal. If we choose to generate `y` before `x` in our
 example we will have no defining constraints for `y` and so we pick a value for
-it freely. But that renders `x` unsolvable if `y > 9` - which will result in
+it freely. But that may render `x` unsolvable if `y > 9` - which will result in
 the generator failing to generate a value (one could consider backtracking, but
-that is very computationally expensive so _relying_ on it would probably not be
-wise).
+that is very computationally expensive so _relying_ on it would not be wise).
 
 Computing a good choice of variable order that leaves the least room for error
-is obviously undecidable and difficult and we choose instead an explicit
-syntax-directed variable order. Specifically, variable dependency in terms is
-_left-to-right_, meaning that the variables in `x + y <. z` will be solved in
-the order `z -> y -> x`. On top of that there is a constraint `dependsOn y x`
-that allows you to overwrite the order of two variables. Consequently, the
-following constraints will be solved in the order `z -> x -> y`:
+is difficult and we choose instead an explicit syntax-directed variable order.
+Specifically, variable dependency in terms is _left-to-right_, meaning that the
+variables in `x + y <. z` will be solved in the order `z -> y -> x`. On top of
+that there is a constraint `dependsOn y x` that allows you to overwrite the
+order of two variables. Consequently, the following constraints will be solved
+in the order `z -> x -> y`:
 
 ```
   x + y <. z
@@ -479,7 +485,7 @@ The principal problem above is that information that is present in the
 constraints is lost, which would force us to rely on a `suchThat` approach to
 generation - which will become very slow as constraint systems grow.
 
-### Using Match to introduce new variables for subcomponents
+### Using `match` to introduce new variables for subcomponents
 
 A solution to the total definition requirement is to *introduce more variables*.
 We can rewrite the problematic `fst p <. snd p` example below as:
@@ -505,8 +511,8 @@ constraints - these need to be bound somewhere - and (2) the order of
 `fst_ p = x` is important, `p` depends on `x`,  and not the other way
 around.
 
-To do both of these things at the same time we use the `match`  construct
-to the language:
+To do both of these things at the same time we use the `match` construct to the
+language:
 
 ```
 match :: Term (a,b) -> (Term a -> Term b -> Pred) -> Pred
@@ -531,7 +537,6 @@ match p $ \ x y -> x <. y
 
 In previous sections we provided some types for several of the library functions: `constrained`, `match`,
 
-
 ```haskell
 constrained :: HasSpec a => (Term a -> Pred) -> Specification a