main.idr

-- Expected:
--   3
--
-- Actual with Idris 2 0.8.0's default Chez backend:
--   Exception: incorrect number of arguments 0 to #<procedure ...>
                            
data Tail = MkTail (Inf (Nat -> Nat))
                            
mutual                      
  tail : Nat -> Nat         
  tail 0 = 3                
  tail _ = case delayedTail of MkTail delayed => delayed 0
 
  delayedTail : Tail
  delayedTail = MkTail (Delay tail)
 
main : IO ()
main = printLn (tail 1)