diff --git a/README.org b/README.org
index 35bdbdd..322d92c 100644
--- a/README.org
+++ b/README.org
@@ -154,6 +154,16 @@ Available debug flags include:
 - [ ] quicksort (core and rlp)
 - [ ] factorial (core and rlp)
 
+
+
+** TODO [#C] fix spacing in pretty-printing                                :bug:
+   note the extra space before the equals sign:
+   #begin_src
+   >>> makeItPretty $ justInferRlp "id x = x" <&> rlpProgToCore
+   Right 
+   
+   id : ∀ ($a0 : Type). $a0 -> $a0  = <lambda>;
+   #end_src
 * Releases
 
 ** +December Release+
diff --git a/rlp.cabal b/rlp.cabal
index 0d94ca3..388a32d 100644
--- a/rlp.cabal
+++ b/rlp.cabal
@@ -56,6 +56,7 @@ library
                     , Rlp2Core
                     , Control.Monad.Utils
                     , Misc
+                    , Misc.MonadicRecursionSchemes
                     , Misc.Lift1
                     , Misc.CofreeF
                     , Core.SystemF
diff --git a/src/Compiler/JustRun.hs b/src/Compiler/JustRun.hs
index 16b006c..51cf3fd 100644
--- a/src/Compiler/JustRun.hs
+++ b/src/Compiler/JustRun.hs
@@ -13,6 +13,7 @@ module Compiler.JustRun
     , justParseRlp
     , justTypeCheckCore
     , justHdbg
+    , justInferRlp
     , makeItPretty, makeItPretty'
     )
     where
@@ -35,6 +36,7 @@ import Data.Pretty
 
 import Rlp.AltParse
 import Rlp.AltSyntax                    qualified as Rlp
+import Rlp.HindleyMilner
 ----------------------------------------------------------------------------------
 
 justHdbg :: String -> IO GmState
@@ -65,6 +67,12 @@ justTypeCheckCore s = typechk (T.pack s)
                     & rlpcToEither
     where typechk = lexCoreR >=> parseCoreProgR >=> checkCoreProgR
 
+justInferRlp :: String
+              -> Either [MsgEnvelope RlpcError]
+                  (Rlp.Program Rlp.PsName Rlp.TypedRlpExpr')
+justInferRlp s = infr (T.pack s) & rlpcToEither
+    where infr = parseRlpProgR >=> typeCheckRlpProgR
+
 makeItPretty :: (Out a) => Either e a -> Either e (Doc ann)
 makeItPretty = fmap out
 
diff --git a/src/Data/Pretty.hs b/src/Data/Pretty.hs
index 1138d30..eea1875 100644
--- a/src/Data/Pretty.hs
+++ b/src/Data/Pretty.hs
@@ -21,7 +21,7 @@ import Data.String                  (IsString(..))
 import Data.Text.Lens               hiding ((:<))
 import Data.Monoid                  hiding (Sum)
 import Data.Bool
-import Control.Lens
+import Control.Lens                 hiding ((:<))
 
 -- instances
 import Control.Comonad.Cofree
@@ -74,6 +74,10 @@ instance (Out1 f, Out1 g) => Out1 (Sum f g) where
 instance (Out (f (Fix f))) => Out (Fix f) where
     outPrec d (Fix f) = outPrec d f
 
+instance (Out (f (Cofree f a)), Out a) => Out (Cofree f a) where
+    outPrec d (a :< f) = maybeParens (d>0) $
+        hsep [outPrec 0 f, ":", outPrec 0 a]
+
 --------------------------------------------------------------------------------
 
 ttext :: Out t => t -> Doc ann
diff --git a/src/Misc/MonadicRecursionSchemes.hs b/src/Misc/MonadicRecursionSchemes.hs
new file mode 100644
index 0000000..bc959cc
--- /dev/null
+++ b/src/Misc/MonadicRecursionSchemes.hs
@@ -0,0 +1,14 @@
+module Misc.MonadicRecursionSchemes
+    where
+--------------------------------------------------------------------------------
+import Control.Monad
+import Data.Functor.Foldable
+--------------------------------------------------------------------------------
+
+-- | catamorphism
+cataM :: (Monad m, Traversable (Base t), Recursive t)
+      => (Base t a -> m a) -- ^ algebra
+      -> t -> m a
+cataM phi = h
+  where h = phi <=< mapM h . project
+
diff --git a/src/Rlp/AltSyntax.hs b/src/Rlp/AltSyntax.hs
index a69e781..c3db52d 100644
--- a/src/Rlp/AltSyntax.hs
+++ b/src/Rlp/AltSyntax.hs
@@ -9,6 +9,7 @@ module Rlp.AltSyntax
     , pattern IntT, pattern TypeT
     , Core.Rec(..)
 
+    , TypedRlpExpr'
     , AnnotatedRlpExpr, TypedRlpExpr
     , TypeF(..)
 
@@ -27,6 +28,7 @@ module Rlp.AltSyntax
 
     -- * Misc
     , serialiseCofree
+    , fixCofree
     )
     where
 --------------------------------------------------------------------------------
@@ -40,7 +42,7 @@ import GHC.Generics             ( Generic, Generic1
 import Data.Hashable
 import Data.Hashable.Lifted
 import GHC.Exts                 (IsString)
-import Control.Lens             hiding ((.=))
+import Control.Lens             hiding ((.=), (:<))
 
 import Data.Functor.Extend
 import Data.Functor.Foldable.TH
@@ -58,6 +60,7 @@ import Core.Syntax              qualified as Core
 type RlpExpr' = RlpExpr PsName
 type RlpExprF' = RlpExprF PsName
 type AnnotatedRlpExpr' = Cofree (RlpExprF PsName)
+type TypedRlpExpr' = TypedRlpExpr PsName
 type Type' = Type PsName
 
 type AnnotatedRlpExpr b = Cofree (RlpExprF b)
@@ -313,3 +316,11 @@ serialiseCofree = cata \case
     ann :<$ e -> object [ "ann" .= ann
                         , "val" .= toJSON1 e ]
 
+--------------------------------------------------------------------------------
+
+fixCofree :: (Functor f, Functor g)
+          => Iso (Fix f) (Fix g) (Cofree f ()) (Cofree g b)
+fixCofree = iso sa bt where
+    sa = foldFix (() :<)
+    bt (_ :< f) = Fix (bt <$> f)
+
diff --git a/src/Rlp/HindleyMilner.hs b/src/Rlp/HindleyMilner.hs
index ec508b4..cb957d5 100644
--- a/src/Rlp/HindleyMilner.hs
+++ b/src/Rlp/HindleyMilner.hs
@@ -144,15 +144,6 @@ gather (InR (CaseEF (te,je) as)) = do
         j = je <> foldOf (each . _2) as' <> eqs
     pure (t,j)
 
--- gather (InR (CaseEF (te,je) [Alter (ConP' n bs) (ta,ja)])) = do
---     -- let tc' be the type of the saturated type constructor
---     tc' <- freshTv
---     bs <- for bs (\b -> (b ^. singular _VarP,) <$> freshTv)
---     let tbs = bs ^.. each . _2
---         tc = foldr (:->) tc' tbs
---         j = equal te tc' <> je <> assume n tc <> forBinds elim bs ja
---     pure (ta,j)
-
 gatherAlter :: (Unique :> es)
             => Type'
             -> Alter PsName (Type', Judgement)
diff --git a/src/Rlp2Core.hs b/src/Rlp2Core.hs
index 7ef5b26..72b7b32 100644
--- a/src/Rlp2Core.hs
+++ b/src/Rlp2Core.hs
@@ -26,11 +26,13 @@ import Data.Function                    (on)
 import GHC.Stack
 import Debug.Trace
 import Numeric
+import Misc.MonadicRecursionSchemes
 
 import Data.Fix                         hiding (cata, para, cataM)
 import Data.Functor.Bind
 import Data.Functor.Foldable
 import Control.Comonad
+import Control.Comonad.Cofree
 
 import Effectful.State.Static.Local
 import Effectful.Labeled
@@ -82,27 +84,72 @@ runNameSupply :: Text -> Eff (NameSupply ': es) a -> Eff es a
 runNameSupply pre = runLabeled $ evalState [ pre <> "_" <> tshow name | name <- [0..] ]
     where tshow = T.pack . show
 
+single :: (Monoid s, Applicative f) => ASetter s t a (f b) -> b -> t
+single l a = mempty & l .~ pure a
+
 -- the rl' program is desugared by desugaring each declaration as a separate
 -- program, and taking the monoidal product of the lot :3
 
 rlpProgToCore :: Rlp.Program PsName (TypedRlpExpr PsName) -> Core.Program Var
 rlpProgToCore = foldMapOf (programDecls . each) declToCore
 
-declToCore :: Rlp.Decl PsName (TypedRlpExpr PsName) -> Core.Program Var
+--------------------------------------------------------------------------------
+
+declToCore :: Rlp.Decl PsName TypedRlpExpr' -> Core.Program Var
 
 -- assume full eta-expansion for now
-declToCore (FunD b [] e) = mempty & programScDefs .~ [ScDef b' [] undefined]
-    where
-        b' = MkVar b (typeToCore $ extract e)
-        e' = runPureEff . runNameSupply b . exprToCore $ e
+declToCore (FunD b [] e) = single programScDefs $
+    ScDef b' [] e'
+  where
+    b' = MkVar b (typeToCore $ extract e)
+    e' = runPureEff . runNameSupply b . cataM exprToCore . retype $ e
+
+dummyExpr :: Text -> Core.Expr b
+dummyExpr a = Var ("<" <> a <> ">")
+
+--------------------------------------------------------------------------------
+
+-- | convert rl' types to Core types, annotate binders, and strip excess type
+-- info.
+retype :: Cofree RlpExprF' (Rlp.Type PsName) -> RlpExpr Var
+retype = (_extract %~ unquantify) >>> fmap typeToCore >>> cata \case
+    t :<$ InL (LamF bs e)
+        -> Finl (LamF bs' e)
+      where
+        bs' = zipWith MkVar bs (t ^.. arrowStops)
+
+    t :<$ InL (VarF n)
+        -> Finl (VarF n)
+
+    t :<$ InR (LetEF r bs e)
+        -> Finr (LetEF r _ _)
+
+unquantify :: Rlp.Type b
+           -> Rlp.Type b
+unquantify (ForallT _ x) = unquantify x
+unquantify x             = x
 
 typeToCore :: Rlp.Type PsName -> Core.Type
-typeToCore (VarT n) = TyVar n
+typeToCore = cata \case
+    VarTF n   -> TyVar n
+    ConTF n   -> TyCon n
+    FunTF     -> TyFun
+    AppTF f x -> TyApp f x
+    -- TODO: we assume all quantified tyvars are of kind Type
+    ForallTF x m -> TyForall (MkVar x TyKindType) m
+
+--------------------------------------------------------------------------------
 
 exprToCore :: (NameSupply :> es)
-           => TypedRlpExpr PsName
-           -> Eff es (Cofree (Core.ExprF Var) Core.Type)
-exprToCore = undefined
+           => RlpExprF Var (Core.Expr Var)
+           -> Eff es (Core.Expr Var)
+
+exprToCore (InL e) = pure . embed $ e
+exprToCore (InR _) = _
+
+exprToCore _ = pure $ dummyExpr "expr"
+
+--------------------------------------------------------------------------------
 
 annotateVar :: Core.Type -> Core.ExprF PsName a -> Core.ExprF Var a