diff --git a/lib/Haskell/Extra/Delay.agda b/lib/Haskell/Extra/Delay.agda
new file mode 100644
index 00000000..46b9d38f
--- /dev/null
+++ b/lib/Haskell/Extra/Delay.agda
@@ -0,0 +1,9 @@
+{-# OPTIONS --sized-types #-}
+
+module Haskell.Extra.Delay where
+
+open import Haskell.Prim.Thunk
+
+data Delay (a : Set) (@0 i : Size) : Set where
+  now : a → Delay a i
+  later : Thunk (Delay a) i → Delay a i
diff --git a/src/Agda2Hs/Compile/Term.hs b/src/Agda2Hs/Compile/Term.hs
index 02478622..63a931ac 100644
--- a/src/Agda2Hs/Compile/Term.hs
+++ b/src/Agda2Hs/Compile/Term.hs
@@ -63,6 +63,8 @@ isSpecialCon = prettyShow >>> \case
   "Haskell.Prim.Tuple._,_"         -> Just tupleTerm
   "Haskell.Prim.Tuple._×_×_._,_,_" -> Just tupleTerm
   "Haskell.Extra.Erase.Erased"     -> Just (\_ _ _ -> erasedTerm)
+  "Haskell.Extra.Delay.Delay.now"   -> Just $ \_ _ -> compileErasedApp
+  "Haskell.Extra.Delay.Delay.later" -> Just $ \_ _ -> compileErasedApp
   _ -> Nothing
 
 tupleTerm :: ConHead -> ConInfo -> Elims -> C (Hs.Exp ())
diff --git a/src/Agda2Hs/Compile/Type.hs b/src/Agda2Hs/Compile/Type.hs
index 2c775b4e..ac2507c1 100644
--- a/src/Agda2Hs/Compile/Type.hs
+++ b/src/Agda2Hs/Compile/Type.hs
@@ -44,6 +44,7 @@ isSpecialType = prettyShow >>> \case
   "Haskell.Prim.Tuple._×_"   -> Just tupleType
   "Haskell.Prim.Tuple._×_×_" -> Just tupleType
   "Haskell.Extra.Erase.Erase" -> Just erasedType
+  "Haskell.Extra.Delay.Delay" -> Just delayType
   _ -> Nothing
 
 tupleType :: QName -> Elims -> C (Hs.Type ())
@@ -55,6 +56,12 @@ tupleType q es = do
 erasedType :: QName -> Elims -> C (Hs.Type ())
 erasedType _ _ = return $ Hs.TyTuple () Hs.Boxed []
 
+delayType :: QName -> Elims -> C (Hs.Type ())
+delayType _ (Apply a : _) = compileType (unArg a)
+delayType _ (_ : _) = __IMPOSSIBLE__
+delayType _ [] = genericDocError =<< text "Cannot compile unapplied Delay type"
+
+
 -- | Add a class constraint to a Haskell type.
 constrainType
   :: Hs.Asst () -- ^ The class assertion.
diff --git a/test/AllTests.agda b/test/AllTests.agda
index a606ff58..b4328359 100644
--- a/test/AllTests.agda
+++ b/test/AllTests.agda
@@ -67,6 +67,7 @@ import Coerce
 import Inlining
 import EraseType
 import Issue257
+import Delay
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -133,4 +134,5 @@ import ModuleParametersImports
 import Coerce
 import Inlining
 import EraseType
+import Delay
 #-}
diff --git a/test/Delay.agda b/test/Delay.agda
new file mode 100644
index 00000000..b74ec943
--- /dev/null
+++ b/test/Delay.agda
@@ -0,0 +1,23 @@
+
+module Delay where
+
+open import Haskell.Prelude
+open import Haskell.Prim.Thunk
+open import Haskell.Extra.Delay
+
+open import Agda.Builtin.Size
+
+postulate
+  div : Int → Int → Int
+  mod : Int → Int → Int
+
+even : Int → Bool
+even x = mod x 2 == 0
+
+collatz : ∀ {@0 j} → Int → Delay Int j
+collatz x = 
+  if x == 0 then now 0
+  else if even x then later (λ where .force → collatz (div x 2))
+  else later λ where .force → collatz (3 * x + 1)
+
+{-# COMPILE AGDA2HS collatz #-}
diff --git a/test/golden/AllTests.hs b/test/golden/AllTests.hs
index d69d9254..d38a514a 100644
--- a/test/golden/AllTests.hs
+++ b/test/golden/AllTests.hs
@@ -64,4 +64,5 @@ import ModuleParametersImports
 import Coerce
 import Inlining
 import EraseType
+import Delay
 
diff --git a/test/golden/Delay.hs b/test/golden/Delay.hs
new file mode 100644
index 00000000..6eeaad90
--- /dev/null
+++ b/test/golden/Delay.hs
@@ -0,0 +1,7 @@
+module Delay where
+
+collatz :: Int -> Int
+collatz x
+  = if x == 0 then 0 else
+      if even x then collatz (div x 2) else collatz (3 * x + 1)
+