type 'a notok = 'a -> 'a notok
- (In the technical jargon, OCaml has isorecursive not equirecursive types.) In any case, the reason that OCaml rejects b, e, and g is not the mere fact that they involve self-application, but the fact that typing them would require constructing one of the kinds of infinite chains of unbroken arrows that OCaml forbids. In case c, we can already see that the type of `f` is acceptable (it was ok in case a), and the self-application doesn't impose any new typing constraints because it never returns, so it can have any result type at all.
+ (In the technical jargon, OCaml has isorecursive not equirecursive types.) In any case, the reason that OCaml rejects b is not the mere fact that it involves self-application, but the fact that typing it would require constructing one of the kinds of infinite chains of unbroken arrows that OCaml forbids. In case c, we can already see that the type of `f` is acceptable (it was ok in case a), and the self-application doesn't impose any new typing constraints because it never returns, so it can have any result type at all.
- In case g, the typing fails not specifically because of a self-application, but because OCaml has already determined that `f` has to take a `()` argument, and even before settling on `f`'s final type, one thing it knows about `f` is that it isn't `()`. So `let rec f () = f () in f f` fails for the same reason that `let rec f () = f () in f id` would.
+ In cases e and g, the typing fails not specifically because of a self-application, but because OCaml has already determined that `f` has to take a `()` argument, and even before settling on `f`'s final type, one thing it knows about `f` is that it isn't `()`. So `let rec f () = f () in f f` fails for the same reason that `let rec f () = f () in f id` would.
24. Throughout this problem, assume that we have: