I am trying to use a data types a la carte approach to define a free monad for templating purposes. I am using Edward Kmett's free package, and a module implementing data types a la carte's injections, modelled on the IOSpec Types module. I have written a few combinators, but I am stuck. My program keeps diverging, and I don't see why. Consider: math :: Math :<: f => MathExpr a -> Free f () blank :: f :<: (Textual :+: Math) => Free f () -> Free (Blank k f) () equals :: Free (Math :+: (Blank L Math)) () -> Free (Math :+: (Blank R Math)) () -> Free Equation () The intention is that a blank takes in a properly typed abstract syntax tree and tags it with "blank k", so that the parsers/renderers do the "right thing" (when I get around to implementing them) The composition (blank . math) has the type: blank . math :: ( f :<: (Textual :+: Math) , Math :<: f ) => MathExpr a -> Free (Blank k f) () Notice that f must be simultaneously less than or equal to the join of Textual and Math, and greater than or equal to Math. So the only possibility for f is Math. (I realize the compiler can't infer this without more work on my part) The problem happens when I try to evaluate (using scoped type signatures to get around my comment above): test :: Free Equation () test = (hoistFree (inj :: Blank 'L Math a -> (Math :+: Blank 'L Math) a) . blank . (math :: MathExpr x -> Free Math ()) $ "hi" ) `equals` (math $ "world") which apparently loops, pegging my CPU at 100%. The computation prints its result as: Free (Equation (Free (DirectSum {unDirectSum = Right at which point the value is truncated and GHCi quits. So it apparently gets as far as figuring out that the first argument to equals is in the latter part of the direct sum, but it doesn't seem t be able to compute blank. Relatively minimal source is available at: monad: http://lpaste.net/93471 data types a la carte: http://lpaste.net/93472 All my functions are total and I don't see a bottom here, but I was never any good at fixed point combinators. Any ideas?