This is a regionalized or "benign" effect. To the degree that this can be proven in Haskell's synthetic effect calculus it's OK. Since Haskell does have `unsafePerformIO` we can, with great care, introduce new rules to the type system. This is how `ST` was created

    -- we need a primitive first
    while :: Monad m => m Bool -> m a -> m ()
    while conde bodye = do
      cond <- conde
      if cond then bodye else return ()

    -- then we can make a direct, verified pure translation
    f :: a -> Int
    f x = runST $ do
      i <- newSTRef 17
      while (readSTRef i >>= \ival -> return (ival > 0)) $ do
        modifySTRef i (\ival -> ival - 1)
      ival <- readSTRef i
      return ival