--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/IdAgda.agda	Thu Dec 12 17:41:03 2019 +0900
@@ -0,0 +1,6 @@
+module IdAgda where
+
+  idAgda : ∀ {A : Set} → A → A
+  idAgda x = x
+
+  {-# COMPILE GHC idAgda as idAgdaFromHs #-}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/foreign.agda	Thu Dec 12 17:41:03 2019 +0900
@@ -0,0 +1,51 @@
+module foreign where
+
+{-# FOREIGN GHC import Data.Maybe #-}
+
+{-# FOREIGN GHC
+  data Foo = Foo | Bar Foo
+
+  countBars :: Foo -> Integer
+  countBars Foo = 0
+  countBars (Bar f) = 1 + countBars f
+#-}
+
+{-# FOREIGN GHC import qualified System.IO #-}
+
+postulate FileHandle : Set
+{-# COMPILE GHC FileHandle = type System.IO.Handle #-}
+
+data Maybe (A : Set) : Set where
+  nothing : Maybe A
+  just    : A → Maybe A
+
+{-# COMPILE GHC Maybe = data Maybe (Nothing | Just) #-}
+
+open import Agda.Builtin.IO
+open import Agda.Builtin.String
+open import Agda.Builtin.Unit
+
+{-# FOREIGN GHC
+  import qualified Data.Text.IO as Text
+  import qualified System.IO as IO
+#-}
+
+postulate
+  stdout    : FileHandle
+  hPutStrLn : FileHandle → String → IO ⊤
+{-# COMPILE GHC stdout    = IO.stdout #-}
+{-# COMPILE GHC hPutStrLn = Text.hPutStrLn #-}
+
+postulate
+  ioReturn : {A : Set} → A → IO A
+
+{-# COMPILE GHC ioReturn = \ _ x -> return x #-}
+
+open import Level
+
+data Either {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
+  left  : A → Either A B
+  right : B → Either A B
+
+{-# FOREIGN GHC type AgdaEither a b = Either #-}
+{-# COMPILE GHC Either = data AgdaEither (Left | Right) #-}