[Haskell-cafe] Type class constraints in rewrite rules

[Janus Troelsen]

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