+ f' = \p. \s. ((error "...") |> g1) s
+ f = f' |> (String -> g2)
+
+Discard args for bottomming function
+
+ f' = \p. \s. ((error "...") |> g1 |> g3
+ g3 :: (S -> (S,T)) ~ (S,T)
+
+Extrude g1.g3
+
+ f'' = \p. \s. (error "...")
+ f' = f'' |> (String -> S -> g1.g3)
+
+And now we can repeat the whole loop. Aargh! The bug is in applying the
+state hack to a function which then swallows the argument.
+
+
+-------------------- Main arity code ----------------------------
+\begin{code}
+-- If e has ArityType (AT n r), then the term 'e'
+-- * Must be applied to at least n *value* args
+-- before doing any significant work
+-- * It will not diverge before being applied to n
+-- value arguments
+-- * If 'r' is ABot, then it guarantees to diverge if
+-- applied to n arguments (or more)
+
+data ArityType = AT Arity ArityRes
+data ArityRes = ATop -- Know nothing
+ | ABot -- Diverges
+
+vanillaArityType :: ArityType
+vanillaArityType = AT 0 ATop -- Totally uninformative
+
+incArity :: ArityType -> ArityType
+incArity (AT a r) = AT (a+1) r
+
+decArity :: ArityType -> ArityType
+decArity (AT 0 r) = AT 0 r
+decArity (AT a r) = AT (a-1) r
+
+andArityType :: ArityType -> ArityType -> ArityType -- Used for branches of a 'case'
+andArityType (AT a1 ATop) (AT a2 ATop) = AT (a1 `min` a2) ATop
+andArityType (AT _ ABot) (AT a2 ATop) = AT a2 ATop
+andArityType (AT a1 ATop) (AT _ ABot) = AT a1 ATop
+andArityType (AT a1 ABot) (AT a2 ABot) = AT (a1 `max` a2) ABot
+
+trimArity :: Bool -> ArityType -> ArityType
+-- We have something like (let x = E in b), where b has the given
+-- arity type. Then
+-- * If E is cheap we can push it inside as far as we like
+-- * If b eventually diverges, we allow ourselves to push inside
+-- arbitrarily, even though that is not quite right
+trimArity _cheap (AT a ABot) = AT a ABot
+trimArity True (AT a ATop) = AT a ATop
+trimArity False (AT _ ATop) = AT 0 ATop -- Bale out
+
+---------------------------
+arityType :: Bool -> CoreExpr -> ArityType