diff --git a/src/Compiler/RLPC.hs b/src/Compiler/RLPC.hs
index e1e6778..5e69e16 100644
--- a/src/Compiler/RLPC.hs
+++ b/src/Compiler/RLPC.hs
@@ -13,10 +13,12 @@ errors and the family of RLPC monads.
 {-# LANGUAGE DeriveGeneric, DerivingStrategies, DerivingVia #-}
 module Compiler.RLPC
     ( RLPC
-    , RLPCT
+    , RLPCT(..)
     , RLPCIO
     , RLPCOptions(RLPCOptions)
     , RlpcError(..)
+    , IsRlpcError(..)
+    , rlpc
     , addFatal
     , addWound
     , MonadErrorful
@@ -135,6 +137,9 @@ addRlpcWound = addWound . liftRlpcErr
 addRlpcFatal :: (IsRlpcError e, Monad m) => e -> RLPCT RlpcError m ()
 addRlpcFatal = addWound . liftRlpcErr
 
+rlpc :: (Monad m) => ErrorfulT e m a -> RLPCT e m a
+rlpc = RLPCT . ReaderT . const
+
 ----------------------------------------------------------------------------------
 
 instance Default RLPCOptions where
diff --git a/src/Core/HindleyMilner.hs b/src/Core/HindleyMilner.hs
index 15b8ab9..d7277c4 100644
--- a/src/Core/HindleyMilner.hs
+++ b/src/Core/HindleyMilner.hs
@@ -7,7 +7,8 @@ module Core.HindleyMilner
     ( Context'
     , infer
     , check
-    , checkProg
+    , checkCoreProg
+    , checkCoreProgR
     , TypeError(..)
     , HMError
     )
@@ -47,6 +48,10 @@ data TypeError
     | TyErrMissingTypeSig Name
     deriving (Show, Eq)
 
+-- TODO:
+instance IsRlpcError TypeError where
+    liftRlpcErr = RlpcErr . show
+
 -- | Synonym for @Errorful [TypeError]@. This means an @HMError@ action may
 -- throw any number of fatal or nonfatal errors. Run with @runErrorful@.
 type HMError = Errorful TypeError
@@ -69,8 +74,8 @@ check g t1 e = do
 
 -- | Typecheck program. I plan to allow for *some* inference in the future, but
 -- in the mean time all top-level binders must have a type annotation.
-checkProg :: Program' -> HMError ()
-checkProg p = scDefs
+checkCoreProg :: Program' -> HMError ()
+checkCoreProg p = scDefs
             & traverse_ k
     where
         scDefs = p ^. programScDefs
@@ -82,8 +87,11 @@ checkProg p = scDefs
              Nothing -> addFatal $ TyErrMissingTypeSig scname
              where scname = sc ^. _lhs._1
 
-checkRlpcProg :: Program' -> RLPC TypeError ()
-checkRlpcProg = undefined
+-- | @checkCoreProgR p@ returns @p@ if @p@ successfully typechecks.
+checkCoreProgR :: Program' -> RLPC RlpcError Program'
+checkCoreProgR p = do
+    liftRlpcErrs . rlpc . checkCoreProg $ p
+    pure p
 
 -- | Infer the type of an expression under some context.
 --
diff --git a/src/Core/TH.hs b/src/Core/TH.hs
index 063d4fe..7d85bf5 100644
--- a/src/Core/TH.hs
+++ b/src/Core/TH.hs
@@ -5,6 +5,7 @@ Description : Core quasiquoters
 module Core.TH
     ( coreExpr
     , coreProg
+    , coreProgT
     , core
     )
     where
@@ -18,8 +19,11 @@ import Data.Default.Class           (def)
 import Data.Text                    qualified as T
 import Core.Parse
 import Core.Lex
+import Core.HindleyMilner           (checkCoreProgR)
 ----------------------------------------------------------------------------------
 
+-- TODO: write in terms of a String -> QuasiQuoter
+
 core :: QuasiQuoter
 core = QuasiQuoter
     { quoteExp = qCore
@@ -44,6 +48,15 @@ coreExpr = QuasiQuoter
     , quoteDec = error "core quasiquotes may only be used in expressions"
     }
 
+-- | Type-checked @coreProg@
+coreProgT :: QuasiQuoter
+coreProgT = QuasiQuoter
+    { quoteExp = qCoreProgT
+    , quotePat = error "core quasiquotes may only be used in expressions"
+    , quoteType = error "core quasiquotes may only be used in expressions"
+    , quoteDec = error "core quasiquotes may only be used in expressions"
+    }
+
 qCore :: String -> Q Exp
 qCore s = case parse (T.pack s) of
     Left e       -> error (show e)
@@ -59,9 +72,16 @@ qCoreExpr s = case parseExpr (T.pack s) of
         parseExpr = evalRLPC def . (lexCore >=> parseCoreExpr)
 
 qCoreProg :: String -> Q Exp
-qCoreProg s = case parseProg (T.pack s) of
+qCoreProg s = case parse (T.pack s) of
     Left e       -> error (show e)
     Right (m,ts) -> lift m
     where
-        parseProg = evalRLPC def . (lexCoreR >=> parseCoreProgR)
+        parse = evalRLPC def . (lexCoreR >=> parseCoreProgR)
+
+qCoreProgT :: String -> Q Exp
+qCoreProgT s = case parse (T.pack s) of
+    Left e      -> error (show e)
+    Right (m,_) -> lift m
+    where
+        parse = evalRLPC def . (lexCoreR >=> parseCoreProgR >=> checkCoreProgR)