For example, any recursive function that uses a typed monadic bind has this issue. The computation is run twice at each level: once to check that the type is correct, and once to continue as normal.
The identity monad with a trivial loop shows this.
let m a = a
let bind (type a b) (x : m a) (f : a -> m b) : m b = f x
let return (type a) (a : a) : m a = a
let rec loop x =
if x <= 0
then return int 0
else bind unit int (return unit {}) (fun _ -> loop (x - 1))
For example, any recursive function that uses a typed monadic
bindhas this issue. The computation is run twice at each level: once to check that the type is correct, and once to continue as normal.The identity monad with a trivial loop shows this.