Hi, I am trying to speed up some code using the Simplicity library by roconnor. He suggested I apply a rewrite rule to implement the full-adder using Haskell's addition:

fullAdder @(Kleisli m) w into Kleisli (\((a,b),c) -> return $ let sum = fromWord w a + fromWord w b + fromWord1 c in (toBit (sum >= 2 ^ wordSize w), toWord w sum))

I turned that description into a rewrite rule by prepending "forall m w.". But that results in "Forall'd variable ‘m’ does not appear on left hand side" and "Not in scope: type variable ‘m’" (which seems contradictory?) So I thought, OK, typically Type Applications are not necessary, I will just remove it. So the RULE becomes: "fullAdderOpt" forall w. fullAdder w = Kleisli (\((a,b),c) -> return $ let sum = fromWord w a + fromWord w b + fromWord1 c in (toBit (sum >= 2 ^ wordSize w), toWord w sum)) but compiling that, I get:

Could not deduce (Monad m) arising from a use of ‘return’". Possible fix: add (Monad m) to the context of the RULE "fullAdderOpt"

OK, that must mean I should prepend "(Monad m) =>". I tried inserting that either before or after the forall, but both variants are parse errors. So I am suspecting a GHC bug, since I was suggested to do something that doesn't parse. But really, I am just wondering how to make a rewrite rule that does what roconnor suggested. The full source code of the final version is here: https://hushfile.it/api/file?fileid=5dc706576e329 Regards, Janus