diff --git a/examples/NanoFeldspar/Core.hs b/examples/NanoFeldspar/Core.hs
--- a/examples/NanoFeldspar/Core.hs
+++ b/examples/NanoFeldspar/Core.hs
@@ -148,7 +148,8 @@
 
 -- | A predicate deciding which constructs can be shared. Lambdas and literals are not shared.
 canShare :: ASTF (FODomain FeldSyms Typeable Top) a -> Maybe (Dict (Top a))
-canShare (prjP (P::P (CLambda Top))      -> Just _) = Nothing
+canShare (lam :$ _)
+    | Just _ <- prjP (P::P (CLambda Top)) lam = Nothing
 canShare (prj -> Just (Literal _)) = Nothing
 canShare _  = Just Dict
 
diff --git a/src/Language/Syntactic/Constructs/Binding/HigherOrder.hs b/src/Language/Syntactic/Constructs/Binding/HigherOrder.hs
--- a/src/Language/Syntactic/Constructs/Binding/HigherOrder.hs
+++ b/src/Language/Syntactic/Constructs/Binding/HigherOrder.hs
@@ -12,7 +12,7 @@
     , HODomain
     , FODomain
     , CLambda
-    , lambda
+    , IsHODomain (..)
     , reifyM
     , reifyTop
     , reify
@@ -47,16 +47,19 @@
 
 
 
--- | Lambda binding
-lambda
-    :: (p (a -> b), p a, pVar a)
-    => (ASTF (HODomain dom p pVar) a -> ASTF (HODomain dom p pVar) b)
-    -> ASTF (HODomain dom p pVar) (a -> b)
-lambda = injC . HOLambda
+-- | An abstraction of 'HODomain'
+class IsHODomain dom p pVar | dom -> p pVar
+  where
+    lambda :: (p (a -> b), p a, pVar a) => (ASTF dom a -> ASTF dom b) -> ASTF dom (a -> b)
 
+instance IsHODomain (HODomain dom p pVar) p pVar
+  where
+    lambda = injC . HOLambda
+
 instance
-    ( Syntactic a, Domain a ~ HODomain dom p pVar
-    , Syntactic b, Domain b ~ HODomain dom p pVar
+    ( Syntactic a, Domain a ~ dom
+    , Syntactic b, Domain b ~ dom
+    , IsHODomain dom p pVar
     , p (Internal a -> Internal b)
     , p (Internal a)
     , pVar (Internal a)
diff --git a/src/Language/Syntactic/Frontend/Monad.hs b/src/Language/Syntactic/Frontend/Monad.hs
--- a/src/Language/Syntactic/Frontend/Monad.hs
+++ b/src/Language/Syntactic/Frontend/Monad.hs
@@ -19,64 +19,63 @@
 
 
 
--- TODO Unfortunately, this module hard-codes the use of `Typeable`. The problem
---      is this: Say we replace `Typeable` in the definition of `Mon` by a
---      parameter `p`. Then `sugarMonad` will get a constraint `p (a -> m r)`.
---      But `r` existentially quantified and can only be constrained in the
---      definition of `Mon`. With `Typeable` this works because
+-- TODO Unfortunately, this module hard-codes the use of `Typeable`. The problem is this: Say we
+--      replace `Typeable` in the definition of `Mon` by a parameter `p`. Then `sugarMonad` will get
+--      a constraint `p (a -> m r)`. But `r` existentially quantified and can only be constrained in
+--      the definition of `Mon`. With `Typeable` this works because
 --      `(Typeable1 m, Typeable a, Typeable r)` implies `Typeable (a -> m r)`.
 
 -- | User interface to embedded monadic programs
-newtype Mon dom pVar m a
+newtype Mon dom m a
   where
     Mon
-        :: { unMon :: forall r
-                   .  (Monad m, Typeable r, InjectC (MONAD m) dom (m r))
-                   => Cont (ASTF (HODomain dom Typeable pVar) (m r)) a
+        :: { unMon
+              :: forall r . (Monad m, Typeable r, InjectC (MONAD m) dom (m r))
+              => Cont (ASTF dom (m r)) a
            }
-        -> Mon dom pVar m a
+        -> Mon dom m a
 
-deriving instance Functor (Mon dom pVar m)
+deriving instance Functor (Mon dom m)
 
-instance (Monad m) => Monad (Mon dom pVar m)
+instance (Monad m) => Monad (Mon dom m)
   where
     return a = Mon $ return a
     ma >>= f = Mon $ unMon ma >>= unMon . f
 
 -- | One-layer desugaring of monadic actions
 desugarMonad
-    :: ( InjectC (MONAD m) dom (m a)
+    :: ( IsHODomain dom Typeable pVar
+       , InjectC (MONAD m) dom (m a)
        , Monad m
        , Typeable1 m
        , Typeable a
        )
-    => Mon dom pVar m (ASTF (HODomain dom Typeable pVar) a)
-    -> ASTF (HODomain dom Typeable pVar) (m a)
+    => Mon dom m (ASTF dom a) -> ASTF dom (m a)
 desugarMonad = flip runCont (sugarSymC Return) . unMon
 
 -- | One-layer sugaring of monadic actions
 sugarMonad
-    :: ( Monad m
+    :: ( IsHODomain dom Typeable pVar
+       , Monad m
        , Typeable1 m
        , Typeable a
        , pVar a
        )
-    => ASTF (HODomain dom Typeable pVar) (m a)
-    -> Mon dom pVar m (ASTF (HODomain dom Typeable pVar) a)
+    => ASTF dom (m a) -> Mon dom m (ASTF dom a)
 sugarMonad ma = Mon $ cont $ sugarSymC Bind ma
 
-instance ( Syntactic a
-         , Domain a ~ HODomain dom Typeable pVar
+instance ( Syntactic a, Domain a ~ dom
+         , IsHODomain dom Typeable pVar
          , InjectC (MONAD m) dom (m (Internal a))
          , Monad m
          , Typeable1 m
          , Typeable (Internal a)
          , pVar (Internal a)
          ) =>
-           Syntactic (Mon dom pVar m a)
+           Syntactic (Mon dom m a)
   where
-    type Domain (Mon dom pVar m a)   = Domain a
-    type Internal (Mon dom pVar m a) = m (Internal a)
+    type Domain (Mon dom m a)   = dom
+    type Internal (Mon dom m a) = m (Internal a)
     desugar = desugarMonad . fmap desugar
     sugar   = fmap sugar   . sugarMonad
 
diff --git a/syntactic.cabal b/syntactic.cabal
--- a/syntactic.cabal
+++ b/syntactic.cabal
@@ -1,5 +1,5 @@
 Name:           syntactic
-Version:        1.4
+Version:        1.5.1
 Synopsis:       Generic abstract syntax, and utilities for embedded languages
 Description:    This library provides:
                 .
diff --git a/tests/gold/prog4.txt b/tests/gold/prog4.txt
--- a/tests/gold/prog4.txt
+++ b/tests/gold/prog4.txt
@@ -1,49 +1,43 @@
-Let 4
-|
-+- Lambda 1
-|  |
-|  `- Let 2
-|     |
-|     +- sel1
-|     |  |
-|     |  `- var:1
-|     |
-|     `- Let 3
-|        |
-|        +- sel2
-|        |  |
-|        |  `- var:1
-|        |
-|        `- (*)
-|           |
-|           +- (-)
-|           |  |
-|           |  +- var:2
-|           |  |
-|           |  `- var:3
-|           |
-|           `- (-)
-|              |
-|              +- var:3
-|              |
-|              `- var:2
+Lambda 0
 |
-`- Lambda 0
+`- Let 1
    |
-   `- Let
+   +- tup2
+   |  |
+   |  +- (*)
+   |  |  |
+   |  |  +- var:0
+   |  |  |
+   |  |  `- 2
+   |  |
+   |  `- (*)
+   |     |
+   |     +- var:0
+   |     |
+   |     `- 3
+   |
+   `- Let 2
       |
-      +- tup2
-      |  |
-      |  +- (*)
-      |  |  |
-      |  |  +- var:0
-      |  |  |
-      |  |  `- 2
+      +- sel1
       |  |
-      |  `- (*)
-      |     |
-      |     +- var:0
-      |     |
-      |     `- 3
+      |  `- var:1
       |
-      `- var:4
+      `- Let 3
+         |
+         +- sel2
+         |  |
+         |  `- var:1
+         |
+         `- (*)
+            |
+            +- (-)
+            |  |
+            |  +- var:2
+            |  |
+            |  `- var:3
+            |
+            `- (-)
+               |
+               +- var:3
+               |
+               `- var:2