liquidhaskell-0.4.0.0: tests/pos/Coercion.hs

{-@ LIQUID "--no-termination" @-}

module Encoding where

data F a = F a
data BS = BS (F Int)
bar :: IO (F Int)
bar = undefined

foo = undefined


-- start ::  F Int -> IO BS
start fp = foo fp $ go
  where go ptr = do
         -- ensure :: (IO BS ~ IO b) => IO b -> IO b
         let ensure act
               | False = act
               | otherwise = do
                   fp' <- bar
                   start fp -- ((start fp) `cast` (IO BS ~ IO b)) 
         ensure $ return $ BS fp