| 43 | === Converges detection === |

| 44 | |

| 45 | Nested CPR is only sound if we know that the nested values are known to converge for sure. The semantics is clear: If `f` has CPR `<...>m(tm(),)`, then in the body of `case f x of (a,b)`, when entering `a`, we are guaranteed termination. |

| 46 | |

| 47 | What is the semantics of an outer `t`? Given `f` with CPR `<L>tm()` and `g` with CPR `<S>tm()`? Does the latter even make sense? If so, should `f undefined` have CPR `m()` or `tm()`? Two possibilities: |

| 48 | 1. The convergence information a function is what holds if its strictness annotations are fulfilled: So if `g x` has `tm()` if `x` has `t` (possibly because it has previously been evaluated by the caller), otherwise `m()`. `f x` always has `m ()` (presumably because `x` is _never_ entered when evaluating `f`. |

| 49 | 2. The convergence information a function is what holds always. This would ineffect prevent `<S>tm()` from happening. |

| 50 | |

| 51 | The first is stronger, but more involved. So currently, we go with the second one. |

| 52 | |

| 53 | This means that {{{t `bothRes` m}}} is still `t`! |

| 54 | |