diff --git a/src/Agda/Core/Converter.agda b/src/Agda/Core/Converter.agda
index c40189e..b0da85e 100644
--- a/src/Agda/Core/Converter.agda
+++ b/src/Agda/Core/Converter.agda
@@ -23,6 +23,8 @@ module Agda.Core.Converter
     {{@0 sig     : Signature}}
   where
 
+{-# FOREIGN AGDA2HS import Agda.Core.TCMInstances #-}
+
 private open module @0 G = Globals globals
 
 private variable
diff --git a/src/Agda/Core/Reduce.agda b/src/Agda/Core/Reduce.agda
index 92d411a..bd7ddf9 100644
--- a/src/Agda/Core/Reduce.agda
+++ b/src/Agda/Core/Reduce.agda
@@ -60,27 +60,39 @@ data Frame (@0 α : Scope Name) : Set where
   FProj : (@0 x : Name) → {@(tactic auto) _ : x ∈ defScope} → Frame α
   FCase : (bs : Branches α cs) (m : Type (x ◃ α)) → Frame α
 
+{-# COMPILE AGDA2HS Frame #-}
+
 unFrame : Frame α → Term α → Term α
 unFrame (FApp v) u = TApp u v
 unFrame (FProj f) u = TProj u f
 unFrame (FCase bs m) u = TCase u bs m
 
+{-# COMPILE AGDA2HS unFrame #-}
+
 weakenFrame : α ⊆ β → Frame α → Frame β
 weakenFrame s (FApp u) = FApp (weaken s u)
 weakenFrame s (FProj f) = FProj f
 weakenFrame s (FCase bs m) = FCase (weakenBranches s bs) (weakenType (subBindKeep s) m)
 
+{-# COMPILE AGDA2HS weakenFrame #-}
+
 Stack : (@0 α : Scope Name) → Set
 Stack α = List (Frame α)
 
+{-# COMPILE AGDA2HS Stack #-}
+
 unStack : Stack α → Term α → Term α
 unStack [] u = u
 unStack (f ∷ fs) u = unStack fs (unFrame f u)
 
+{-# COMPILE AGDA2HS unStack #-}
+
 weakenStack : α ⊆ β → Stack α → Stack β
 weakenStack s [] = []
 weakenStack s (f ∷ fs) = weakenFrame s f ∷ weakenStack s fs
 
+{-# COMPILE AGDA2HS weakenStack #-}
+
 record State (@0 α : Scope Name) : Set where
   constructor MkState
   field
diff --git a/src/Agda/Core/Signature.agda b/src/Agda/Core/Signature.agda
index cb7cddf..eecf381 100644
--- a/src/Agda/Core/Signature.agda
+++ b/src/Agda/Core/Signature.agda
@@ -41,7 +41,7 @@ opaque
               → d
   caseTelBind (ExtendTel _ a tel) f = f a tel
 
-
+{-# COMPILE AGDA2HS caseTelEmpty #-}
 {-# COMPILE AGDA2HS caseTelBind #-}
 
 record Constructor (@0 pars : Scope Name) (@0 ixs : Scope Name) (@0 c : Name) (@0 cp  : c ∈ conScope) : Set where
diff --git a/src/Agda/Core/Syntax.agda b/src/Agda/Core/Syntax.agda
index 009acc9..5d38786 100644
--- a/src/Agda/Core/Syntax.agda
+++ b/src/Agda/Core/Syntax.agda
@@ -36,7 +36,7 @@ record Type α where
     typeSort : Sort α
     unType   : Term α
 open Type public
-{-# COMPILE AGDA2HS Type #-}
+{-# COMPILE AGDA2HS Type deriving Show #-}
 
 data Subst : (@0 α β : Scope Name) → Set where
   SNil  : Subst mempty β
@@ -101,7 +101,7 @@ data Branch α where
 data Branches α where
   BsNil : Branches α mempty
   BsCons : Branch α c → Branches α cs → Branches α (c ◃ cs)
-{-# COMPILE AGDA2HS Branches #-}
+{-# COMPILE AGDA2HS Branches deriving Show #-}
 
 opaque
   unfolding Scope
@@ -121,10 +121,12 @@ opaque
 rezzBranches : Branches α β → Rezz β
 rezzBranches BsNil = rezz mempty
 rezzBranches (BsCons {c = c} bh bt) = rezzCong (λ cs → c ◃ cs) (rezzBranches bt)
+{-# COMPILE AGDA2HS rezzBranches #-}
 
 allBranches : Branches α β → All (λ c → c ∈ conScope) β
 allBranches BsNil = allEmpty
 allBranches (BsCons (BBranch _ {ci} _ _) bs) = allJoin (allSingl ci) (allBranches bs)
+{-# COMPILE AGDA2HS allBranches #-}
 
 apply : Term α → Term α → Term α
 apply u v = TApp u v
@@ -229,6 +231,7 @@ weakenSort p (STyp x) = STyp x
 {-# COMPILE AGDA2HS weakenSort #-}
 
 weakenType p (El st t) = El (weakenSort p st) (weaken p t)
+{-# COMPILE AGDA2HS weakenType #-}
 
 weakenBranch p (BBranch c r x) = BBranch c r (weaken (subJoinKeep (rezzCong revScope r) p) x)
 {-# COMPILE AGDA2HS weakenBranch #-}
@@ -262,6 +265,8 @@ concatSubst SNil q =
 concatSubst (SCons v p) q =
   subst0 (λ α → Subst α _) (associativity _ _ _) (SCons v (concatSubst p q))
 
+{-# COMPILE AGDA2HS concatSubst #-}
+
 opaque
   unfolding Scope Sub
 
@@ -271,6 +276,8 @@ opaque
     SCons (TVar x {coerce p inHere})
           (subToSubst (rezz α) (joinSubRight (rezz _) p))
 
+{-# COMPILE AGDA2HS subToSubst #-}
+
 opaque
   unfolding Scope revScope
 
@@ -307,6 +314,7 @@ raiseSubst {β = β} r (SCons {α = α} u e) =
 
 revIdSubst : {@0 α : Scope Name} → Rezz α → α ⇒ ~ α
 revIdSubst {α} r = subst0 (λ s →  s ⇒ (~ α)) (revsInvolution α) (revSubst (idSubst (rezzCong revScope r)))
+{-# COMPILE AGDA2HS revIdSubst #-}
 
 raise : {@0 α β : Scope Name} → Rezz α → Term β → Term (α <> β)
 raise r = weaken (subJoinDrop r subRefl)
diff --git a/src/Agda/Core/Typechecker.agda b/src/Agda/Core/Typechecker.agda
index 8b198d7..cb21fee 100644
--- a/src/Agda/Core/Typechecker.agda
+++ b/src/Agda/Core/Typechecker.agda
@@ -168,6 +168,7 @@ inferData ctx d pars ixs = do
   typars ← checkSubst ctx (weakenTel subEmpty (dataParameterTel dt)) pars
   tyixs ← checkSubst ctx (substTelescope pars (dataIndexTel dt)) ixs
   return (sortType (substSort pars (dataSort dt)) , TyData d dt deq typars tyixs)
+{-# COMPILE AGDA2HS inferData #-}
 
 checkBranch : ∀ {@0 con : Name} (Γ : Context α)
                 (bs : Branch α con)
diff --git a/src/Agda/Core/Typing.agda b/src/Agda/Core/Typing.agda
index a3d8041..cd53b6e 100644
--- a/src/Agda/Core/Typing.agda
+++ b/src/Agda/Core/Typing.agda
@@ -162,6 +162,8 @@ data TyBranches {α} Γ dt ps rt where
            → TyBranches Γ dt ps rt bs
            → TyBranches Γ dt ps rt (BsCons b bs)
 
+{-# COMPILE AGDA2HS TyBranches #-}
+
 data TyBranch {α} Γ dt ps rt where
   TyBBranch : (@0 c : Name) → (c∈dcons : c ∈ dataConstructorScope dt)
             → (let (c∈cons , con ) = dataConstructors dt c)
@@ -177,6 +179,8 @@ data TyBranch {α} Γ dt ps rt where
             → TyTerm (addContextTel ctel Γ) rhs (substType bsubst rt)
             → TyBranch Γ dt ps rt (BBranch c {c∈cons} r rhs)
 
+{-# COMPILE AGDA2HS TyBranch #-}
+
 data TySubst {α} Γ where
   TyNil  : TySubst Γ SNil EmptyTel
   TyCons : {@0 r : Rezz α}