let rec tree_best_sofar (t : 'a color_tree) (lead : maybe_leader) : maybe_leader * int =
match t with
- | Leaf a -> (None, a)
+ | Leaf a -> (lead, a)
| Branch(l, col, r) ->
let (lead',left_score) = tree_best_sofar l lead in
let (lead'',right_score) = tree_best_sofar r lead' in
also a mistake. What we want is a result whose type _is_ `Bool`, that is, `∀α. α -> α -> α`. `(q [Bool])` doesn't have that type, but
rather the type `Bool -> Bool -> Bool`. The first, desired, type has an outermost `∀`. The second, wrong type doesn't; it only has `∀`s
inside the antecedents and consequents of the various arrows. The last one of those could be promoted to be an outermost `∀`, since
- `P -> ∀α. Q ≡ ∀α. P -> Q` when `α` is not free in `P`. But that couldn't be done with the others.
+ `P -> ∀α. Q` is equivalent to `∀α. P -> Q` when `α` is not free in `P`. But that couldn't be done with the others.
The type `Nat` (for "natural number") may be encoded as follows: