diff --git a/src/Agda/Core/Converter.agda b/src/Agda/Core/Converter.agda
index 83187fa..426baae 100644
--- a/src/Agda/Core/Converter.agda
+++ b/src/Agda/Core/Converter.agda
@@ -20,6 +20,7 @@ open import Agda.Core.Context globals
 open import Agda.Core.Conversion globals sig
 open import Agda.Core.Reduce globals
 open import Agda.Core.TCM globals sig
+open import Agda.Core.TCMInstances
 open import Agda.Core.Utils renaming (_,_ to _Σ,_)
 
 open import Haskell.Extra.Erase
@@ -30,6 +31,16 @@ open import Haskell.Law.Equality
 private variable
   @0 α : Scope name
 
+
+reduceTo : {@0 α : Scope name} (r : Rezz _ α) (sig : Signature) (v : Term α) (f : Fuel)
+         → TCM (∃[ t ∈ Term α ] (ReducesTo sig v t))
+reduceTo r sig v f =
+  case reduce r sig v f of λ where
+    Nothing        → tcError "not enough fuel to reduce a term"
+    (Just u) ⦃ p ⦄ → return $ u ⟨ ⟨ r ⟩ f ⟨ p ⟩ ⟩
+{-# COMPILE AGDA2HS reduceTo #-}
+
+
 convVars : ∀ Γ
            (s : Term α)
            (@0 x y : name)
diff --git a/src/Agda/Core/TCM.agda b/src/Agda/Core/TCM.agda
index 2fee8b5..11d612c 100644
--- a/src/Agda/Core/TCM.agda
+++ b/src/Agda/Core/TCM.agda
@@ -50,49 +50,6 @@ tcError : TCError -> TCM a
 tcError = MkTCM ∘ const ∘ Left
 {-# COMPILE AGDA2HS tcError #-}
 
-private
-  fmapTCM : (a → b) → TCM a → TCM b
-  fmapTCM f = MkTCM ∘ fmap (fmap f) ∘ runTCM
-  {-# COMPILE AGDA2HS fmapTCM #-}
-
-  liftA2TCM : (a → b → c) → TCM a → TCM b → TCM c
-  liftA2TCM g ta tb = MkTCM λ e → g <$> runTCM ta e <*> runTCM tb e
-  {-# COMPILE AGDA2HS liftA2TCM #-}
-
-  pureTCM : a → TCM a
-  pureTCM = MkTCM ∘ const ∘ Right
-  {-# COMPILE AGDA2HS pureTCM #-}
-
-  bindTCM : TCM a → (a → TCM b) → TCM b
-  bindTCM ma mf = MkTCM λ f → do v ← runTCM ma f ; runTCM (mf v) f
-  {-# COMPILE AGDA2HS bindTCM #-}
-
-instance
-  iFunctorTCM : Functor TCM
-  iFunctorTCM .fmap  = fmapTCM
-  iFunctorTCM ._<$>_ = fmapTCM
-  iFunctorTCM ._<&>_ = λ x f → fmapTCM f x
-  iFunctorTCM ._<$_  = λ x m → fmapTCM (λ b → x {{b}}) m
-  iFunctorTCM ._$>_  = λ m x → fmapTCM (λ b → x {{b}}) m
-  iFunctorTCM .void  = fmapTCM (const tt)
-  {-# COMPILE AGDA2HS iFunctorTCM #-}
-
-instance
-  iApplicativeTCM : Applicative TCM
-  iApplicativeTCM .pure  = pureTCM
-  iApplicativeTCM ._<*>_ = liftA2TCM id
-  iApplicativeTCM ._<*_  = liftA2TCM (λ z _ → z)
-  iApplicativeTCM ._*>_  = liftA2TCM (λ _ z → z)
-  {-# COMPILE AGDA2HS iApplicativeTCM #-}
-
-instance
-  iMonadTCM : Monad TCM
-  iMonadTCM ._>>=_  = bindTCM
-  iMonadTCM .return = pureTCM
-  iMonadTCM ._>>_   = λ x y → bindTCM x (λ z → y {{z}})
-  iMonadTCM ._=<<_  = flip bindTCM
-  {-# COMPILE AGDA2HS iMonadTCM #-}
-
 liftEither : Either TCError a → TCM a
 liftEither (Left e) = MkTCM λ f → Left e
 liftEither (Right v) = MkTCM λ f → Right v
@@ -104,11 +61,3 @@ liftMaybe Nothing e = MkTCM λ f → Left e
 liftMaybe (Just x) e = MkTCM λ f → Right x
 
 {-# COMPILE AGDA2HS liftMaybe #-}
-
-reduceTo : {@0 α : Scope name} (r : Rezz _ α) (sig : Signature) (v : Term α) (f : Fuel)
-         → TCM (∃[ t ∈ Term α ] (ReducesTo sig v t))
-reduceTo r sig v f =
-  case reduce r sig v f of λ where
-    Nothing        → tcError "not enough fuel to reduce a term"
-    (Just u) ⦃ p ⦄ → return $ u ⟨ ⟨ r ⟩ f ⟨ p ⟩ ⟩
-{-# COMPILE AGDA2HS reduceTo #-}
diff --git a/src/Agda/Core/TCMInstances.agda b/src/Agda/Core/TCMInstances.agda
new file mode 100644
index 0000000..76690e0
--- /dev/null
+++ b/src/Agda/Core/TCMInstances.agda
@@ -0,0 +1,57 @@
+
+
+
+module Agda.Core.TCMInstances where
+
+open import Haskell.Prelude
+open import Agda.Core.GlobalScope
+open import Agda.Core.Signature
+open import Agda.Core.TCM
+
+private variable
+  @0 name : Set
+  @0 globals : Globals name
+  @0 sig : Signature globals
+
+private
+  fmapTCM : (a → b) → TCM globals sig a → TCM globals sig b
+  fmapTCM f = MkTCM ∘ fmap (fmap f) ∘ runTCM
+  {-# COMPILE AGDA2HS fmapTCM #-}
+
+  liftA2TCM : (a → b → c) → TCM globals sig a → TCM globals sig b → TCM globals sig c
+  liftA2TCM g ta tb = MkTCM λ e → g <$> runTCM ta e <*> runTCM tb e
+  {-# COMPILE AGDA2HS liftA2TCM #-}
+
+  pureTCM : a → TCM globals sig a
+  pureTCM = MkTCM ∘ const ∘ Right
+  {-# COMPILE AGDA2HS pureTCM #-}
+
+  bindTCM : TCM globals sig a → (a → TCM globals sig b) → TCM globals sig b
+  bindTCM ma mf = MkTCM λ f → do v ← runTCM ma f ; runTCM (mf v) f
+  {-# COMPILE AGDA2HS bindTCM #-}
+
+instance
+  iFunctorTCM : Functor (TCM globals sig)
+  iFunctorTCM .fmap  = fmapTCM
+  iFunctorTCM ._<$>_ = fmapTCM
+  iFunctorTCM ._<&>_ = λ x f → fmapTCM f x
+  iFunctorTCM ._<$_  = λ x m → fmapTCM (λ b → x {{b}}) m
+  iFunctorTCM ._$>_  = λ m x → fmapTCM (λ b → x {{b}}) m
+  iFunctorTCM .void  = fmapTCM (const tt)
+  {-# COMPILE AGDA2HS iFunctorTCM #-}
+
+instance
+  iApplicativeTCM : Applicative (TCM globals sig)
+  iApplicativeTCM .pure  = pureTCM
+  iApplicativeTCM ._<*>_ = liftA2TCM id
+  iApplicativeTCM ._<*_  = liftA2TCM (λ z _ → z)
+  iApplicativeTCM ._*>_  = liftA2TCM (λ _ z → z)
+  {-# COMPILE AGDA2HS iApplicativeTCM #-}
+
+instance
+  iMonadTCM : Monad (TCM globals sig)
+  iMonadTCM ._>>=_  = bindTCM
+  iMonadTCM .return = pureTCM
+  iMonadTCM ._>>_   = λ x y → bindTCM x (λ z → y {{z}})
+  iMonadTCM ._=<<_  = flip bindTCM
+  {-# COMPILE AGDA2HS iMonadTCM #-}
diff --git a/src/Agda/Core/Typechecker.agda b/src/Agda/Core/Typechecker.agda
index 821aaff..0dafa31 100644
--- a/src/Agda/Core/Typechecker.agda
+++ b/src/Agda/Core/Typechecker.agda
@@ -23,6 +23,7 @@ open import Agda.Core.Typing globals sig
 open import Agda.Core.Reduce globals
 open import Agda.Core.Substitute globals
 open import Agda.Core.TCM globals sig
+open import Agda.Core.TCMInstances
 open import Agda.Core.Converter globals sig
 open import Agda.Core.Utils