diff --git a/rlp.cabal b/rlp.cabal
index eeb2ff6..c8fccb2 100644
--- a/rlp.cabal
+++ b/rlp.cabal
@@ -35,10 +35,10 @@ library
                     , Rlp.AltSyntax
                     , Rlp.AltParse
                     , Rlp.HindleyMilner
+                    , Rlp.HindleyMilner.Visual
                     , Rlp.HindleyMilner.Types
                     , Rlp.Syntax.Backstage
                     , Rlp.Syntax.Types
-                    , Rlp.Syntax.Good
                     -- , Rlp.Parse.Decls
                     , Rlp.Parse
                     , Rlp.Parse.Associate
@@ -56,6 +56,7 @@ library
                     , Control.Monad.Utils
                     , Misc
                     , Misc.Lift1
+                    , Misc.CofreeF
                     , Core.SystemF
 
     build-tool-depends: happy:happy, alex:alex
@@ -87,6 +88,11 @@ library
                     , these >=0.2 && <2.0
                     , free >=5.2
                     , bifunctors >=5.2
+                    , blaze-html
+                    , blaze-markup
+                    , clay
+                    , jmacro
+                    , js-jquery
 
     hs-source-dirs:   src
     default-language: GHC2021
diff --git a/src/Compiler/Types.hs b/src/Compiler/Types.hs
index 3f8a015..d80dc58 100644
--- a/src/Compiler/Types.hs
+++ b/src/Compiler/Types.hs
@@ -27,8 +27,6 @@ import Language.Haskell.TH.Syntax   (Lift)
 
 import Control.Comonad
 import Control.Comonad.Cofree
-import Control.Comonad.Trans.Cofree qualified as Trans.Cofree
-import Control.Comonad.Trans.Cofree (CofreeF)
 import Data.Functor.Apply
 import Data.Functor.Bind
 import Data.Functor.Compose
@@ -40,15 +38,13 @@ import Control.Lens                 hiding ((<<~), (:<))
 
 import Data.List.NonEmpty           (NonEmpty)
 import Data.Function                (on)
+import Misc.CofreeF
 --------------------------------------------------------------------------------
 
 -- | Token wrapped with a span (line, column, absolute, length)
 data Located a = Located SrcSpan a
     deriving (Show, Lift, Functor)
 
-pattern (:<$) :: a -> f b -> Trans.Cofree.CofreeF f a b
-pattern a :<$ b = a Trans.Cofree.:< b
-
 (<~>) :: a -> b -> SrcSpan
 (<~>) = undefined
 
diff --git a/src/Core/Syntax.hs b/src/Core/Syntax.hs
index 5b25db7..1432c93 100644
--- a/src/Core/Syntax.hs
+++ b/src/Core/Syntax.hs
@@ -720,7 +720,7 @@ class HasArrowStops s t a b | s -> a, t -> b, s b -> t, t a -> s where
 
 instance HasArrowStops Type Type Type Type where
     arrowStops k (s :-> t) = (:->) <$> k s <*> arrowStops k t
-    arrowStops k t = k t
+    arrowStops k t         = k t
 
 --------------------------------------------------------------------------------
 
diff --git a/src/Data/Pretty.hs b/src/Data/Pretty.hs
index 5302677..44902e7 100644
--- a/src/Data/Pretty.hs
+++ b/src/Data/Pretty.hs
@@ -41,6 +41,9 @@ class Pretty a where
 rpretty :: (IsString s, Pretty a) => a -> s
 rpretty = fromString . render . pretty
 
+instance Pretty Doc where
+    pretty = id
+
 instance Pretty String where
     pretty = Text.PrettyPrint.text
 
@@ -71,9 +74,6 @@ instance (Pretty1 f, Pretty1 g) => Pretty1 (Sum f g) where
 instance (Pretty (f (Fix f))) => Pretty (Fix f) where
     prettyPrec d (Fix f) = prettyPrec d f
 
--- instance (Pretty1 f) => Pretty (Fix f) where
---     prettyPrec d (Fix f) = prettyPrec1 d f
-
 --------------------------------------------------------------------------------
 
 ttext :: Pretty t => t -> Doc
diff --git a/src/Misc/CofreeF.hs b/src/Misc/CofreeF.hs
new file mode 100644
index 0000000..dd90a38
--- /dev/null
+++ b/src/Misc/CofreeF.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE PatternSynonyms #-}
+module Misc.CofreeF
+    ( pattern (:<$)
+    )
+    where
+--------------------------------------------------------------------------------
+import Control.Comonad.Trans.Cofree qualified as Trans.Cofree
+import Control.Comonad.Trans.Cofree (CofreeF)
+--------------------------------------------------------------------------------
+
+pattern (:<$) :: a -> f b -> Trans.Cofree.CofreeF f a b
+pattern a :<$ b = a Trans.Cofree.:< b
+
diff --git a/src/Rlp/AltSyntax.hs b/src/Rlp/AltSyntax.hs
index 21e56a4..03b8810 100644
--- a/src/Rlp/AltSyntax.hs
+++ b/src/Rlp/AltSyntax.hs
@@ -53,7 +53,7 @@ programDecls = lens (\ (Program ds) -> ds) (const Program)
 data Decl b a = FunD b [Pat b] a
               | DataD b [b] [DataCon b]
               | TySigD b (Type b)
-              deriving Show
+              deriving (Show, Functor)
 
 data DataCon b = DataCon b [Type b]
     deriving (Show, Generic)
@@ -217,3 +217,7 @@ instance (Hashable b) => Hashable1 (ExprF b)
 
 makeBaseFunctor ''Type
 
+instance Core.HasArrowStops (Type b) (Type b) (Type b) (Type b) where
+    arrowStops k (s Core.:-> t) = (Core.:->) <$> k s <*> Core.arrowStops k t
+    arrowStops k t         = k t
+
diff --git a/src/Rlp/HindleyMilner.hs b/src/Rlp/HindleyMilner.hs
index 53e4454..3f0949f 100644
--- a/src/Rlp/HindleyMilner.hs
+++ b/src/Rlp/HindleyMilner.hs
@@ -4,6 +4,7 @@
 module Rlp.HindleyMilner
     ( typeCheckRlpProgR
     , solve
+    , annotate
     , TypeError(..)
     , runHM'
     , HM
@@ -11,6 +12,7 @@ module Rlp.HindleyMilner
     where
 --------------------------------------------------------------------------------
 import Control.Lens             hiding (Context', Context, (:<), para)
+import Control.Lens.Unsound
 import Control.Monad.Errorful
 import Control.Monad.State
 import Control.Monad.Accum
@@ -77,14 +79,27 @@ gather' = \case
         let jtfx = mempty & constraints .~ [Equality tf (tx :-> tfx)]
         pure (tfx, jf <> jx <> jtfx)
 
-    Finl (LamF [b] e) -> do
-        tb <- freshTv
+    Finl (LamF bs e) -> do
+        tbs <- for bs (const freshTv)
         (te,je) <- gather e
-        let cs = maybe [] (fmap $ Equality tb) (je ^. assumptions . at b)
-            as = je ^. assumptions & at b .~ Nothing
+        let cs = concatMap (uncurry . equals $ je ^. assumptions) $ bs `zip` tbs
+            as = foldr H.delete (je ^. assumptions) bs
             j = mempty & constraints .~ cs & assumptions .~ as
-            t = tb :-> te
+            t = foldr (:->) te tbs
         pure (t,j)
+      where
+        equals as b tb = maybe []
+            (fmap $ Equality tb)
+            (as ^. at b)
+
+    -- Finl (LamF [b] e) -> do
+    --     tb <- freshTv
+    --     (te,je) <- gather e
+    --     let cs = maybe [] (fmap $ Equality tb) (je ^. assumptions . at b)
+    --         as = je ^. assumptions & at b .~ Nothing
+    --         j = mempty & constraints .~ cs & assumptions .~ as
+    --         t = tb :-> te
+    --     pure (t,j)
 
 unify :: [Constraint] -> HM Context
 
@@ -122,11 +137,8 @@ infer1 e = do
     g <- unify (j ^. constraints)
     pure $ ifoldrOf (contextVars . itraversed) subst t g
 
-solve = undefined
--- solve g e = do
---     (t,j) <- gather e
---     g' <- unify cs
---     pure $ ifoldrOf (contextVars . itraversed) subst t g'
+solve :: RlpExpr PsName -> HM (Cofree (RlpExprF PsName) (Type PsName))
+solve e = sequenceA $ fixtend (infer1 . wrapFix) e
 
 occurs :: PsName -> Type PsName -> Bool
 occurs n = cata \case
diff --git a/src/Rlp/HindleyMilner/Visual.hs b/src/Rlp/HindleyMilner/Visual.hs
new file mode 100644
index 0000000..1a8a71a
--- /dev/null
+++ b/src/Rlp/HindleyMilner/Visual.hs
@@ -0,0 +1,133 @@
+{-# LANGUAGE LexicalNegation #-}
+{-# LANGUAGE QuasiQuotes #-}
+module Rlp.HindleyMilner.Visual
+    (
+    )
+    where
+--------------------------------------------------------------------------------
+import Control.Monad
+import System.IO
+import Data.Text                        qualified as T
+import Data.Text.IO                     qualified as T
+import Data.Pretty
+import Data.String                      (IsString(..))
+import Data.Foldable
+import Misc.CofreeF
+import Control.Exception
+
+import Data.Functor.Foldable
+
+import Text.Blaze.Html5                 as H
+import Text.Blaze.Html5.Attributes      as A
+import Text.Blaze.Html.Renderer.String
+import Clay                             (Css, (?), px, pct, (**), (|>), (|+)
+                                        , (|~))
+import Clay                             qualified as C
+import Clay.Render                      qualified as C
+import Language.Javascript.JMacro
+import Language.Javascript.JQuery       qualified as JQuery
+
+import Core.Syntax                      as Core
+import Rlp.AltSyntax                    as Rlp
+import Rlp.HindleyMilner
+
+import Prelude hiding ((**))
+--------------------------------------------------------------------------------
+
+type AnnExpr = Cofree (RlpExprF PsName)
+
+tooltips :: Css
+tooltips = do
+    ".has-type" ? do
+        C.position     C.relative
+        C.display      C.inlineBlock
+        C.borderBottom (px 1) C.dotted C.black
+    ".has-type.hovering" ? do
+        C.background C.green
+    ".has-type.hovering" |> ".type-text" ? do
+        C.display      C.block
+        C.opacity      1
+        C.position     C.fixed
+        C.overflowWrap C.breakWord
+    ".has-type" |> ".type-text" ? do
+        C.display      C.none
+        C.overflowWrap C.breakWord
+        C.maxWidth     (pct 50)
+
+stylesheet :: Css
+stylesheet = tooltips
+
+numbers :: Int -> Html
+numbers n = docTypeHtml do
+    H.head do
+        H.title "naturals"
+        H.style "doge"
+    body do
+        pre "a list of nats"
+        ul $ forM_ [1..n] (li . toHtml)
+
+withTooltip :: Html -> Html -> Html
+withTooltip normal hover =
+    H.div ! class_ "has-type"
+        $ normal *> (H.div ! class_ "type-text" $ hover)
+
+-- withTooltip :: Html -> Html -> Html
+-- withTooltip normal hover =
+--     H.div ! class_ "has-type"
+--           -- ! onload "installHoverListener(this)"
+--         $ normal
+
+annExpr :: (ann -> Doc) -> AnnExpr ann -> Html
+annExpr sf = code . cata \case
+    t :<$ InL (LitF l)   -> withTooltip (rpretty l) (sf' t)
+    t :<$ InL (VarF n)   -> withTooltip (rpretty n) (sf' t)
+    t :<$ InL (AppF f x) -> withTooltip (f *> " " *> x) (sf' t)
+    t :<$ InL (LamF bs e) -> withTooltip ("λ" *> bs' *> " -> " *> e) (sf' t)
+        where
+            bs' = fromString . render . hsep $ prettyPrec appPrec1 <$> bs
+  where
+    sf' = fromString . show . sf
+
+rootScript :: JStat
+rootScript = [jmacro|
+    $(".has-type").on("mouseover mouseout", \e {
+        e.stopPropagation();
+        $(this).toggleClass("hovering", e.type === "mouseover");
+        var o = $(this).children(".type-text")[0];
+        var x = e.clientX;
+        var y = e.clientY;
+        o.style.top = (y + 20) + 'px';
+        o.style.left = (x + 20) + 'px';
+    });
+|]
+
+jsScript :: (IsString s, JsToDoc w, JMacro w) => w -> s
+jsScript = fromString . show . renderJs
+
+rootPage :: Html -> Html
+rootPage html = docTypeHtml do
+    H.head do
+        H.title "naturals"
+        H.style (toHtml . C.render $ stylesheet)
+    H.body do
+        html
+        script ! src (fromString $ "https:" ++ JQuery.url) $ ""
+        script ! src "https://code.jquery.com/ui/1.13.2/jquery-ui.min.js" $ ""
+        script (fromString . show . renderJs $ rootScript)
+
+renderTmp :: Html -> IO ()
+renderTmp = writeFile "/tmp/t.html" . renderHtml
+
+renderTmp' :: Html -> IO ()
+renderTmp' = writeFile "/tmp/t.html" . renderHtml . rootPage
+
+renderExpr :: RlpExpr PsName -> IO ()
+renderExpr e = case runHM' . annotate $ e of
+    Left es -> error (show es)
+    Right e' -> renderTmp' . annExpr (fromString . show) $ e'
+
+renderExpr' :: RlpExpr PsName -> IO ()
+renderExpr' e = case runHM' . solve $ e of
+    Left es -> error (show es)
+    Right e' -> renderTmp' . annExpr pretty $ e'
+
diff --git a/src/Rlp/Syntax/Good.hs b/src/Rlp/Syntax/Good.hs
deleted file mode 100644
index 11ae14f..0000000
--- a/src/Rlp/Syntax/Good.hs
+++ /dev/null
@@ -1,56 +0,0 @@
-{-# LANGUAGE TemplateHaskell #-}
-module Rlp.Syntax.Good
-    ( Decl(..), Program(..)
-    , programDecls
-    , Mistake(..)
-    )
-    where
---------------------------------------------------------------------------------
-import Data.Kind
-import Control.Lens
-import Rlp.Syntax.Types (NameP)
-import Rlp.Syntax.Types qualified as Rlp
---------------------------------------------------------------------------------
-
-data Program b a = Program
-    { _programDecls :: [Decl b a]
-    }
-
-data Decl p a = FunD   (NameP p) [Rlp.Pat p] a
-              | TySigD [NameP p] (Rlp.Ty p)
-              | DataD  (NameP p) [NameP p] [Rlp.ConAlt p]
-              | InfixD Rlp.Assoc Int (NameP p)
-
-type Where p a = [Binding p a]
-
-data Binding p a = PatB (Rlp.Pat p) a
-    deriving (Functor, Foldable, Traversable)
-
-makeLenses ''Program
-
-class Mistake a where
-    type family Ammend a :: Type
-    ammendMistake :: a -> Ammend a
-
-instance Mistake (Rlp.Program p a) where
-    type Ammend (Rlp.Program p a) = Program p (Rlp.Expr' p a)
-
-    ammendMistake p = Program
-        { _programDecls = ammendMistake <$> Rlp._programDecls p
-        }
-
-instance Mistake (Rlp.Decl p a) where
-    type Ammend (Rlp.Decl p a) = Decl p (Rlp.Expr' p a)
-
-    ammendMistake = \case
-        Rlp.FunD n as e _  -> FunD n as e
-        Rlp.TySigD ns t    -> TySigD ns t
-        Rlp.DataD n as cs  -> DataD n as cs
-        Rlp.InfixD ass p n -> InfixD ass p n
-
-instance Mistake (Rlp.Binding p a) where
-    type Ammend (Rlp.Binding p a) = Binding p (Rlp.ExprF p a)
-
-    ammendMistake = \case
-        Rlp.PatB k v -> PatB k v
-