| > I think your problem here is that there's no mention of `a' on the | > left-hand size of from_val's type signature; you either need to use | > MPTC+fundep to associate what result is compared to a, or else use a | > phantom type parameter of Val to make it "data Val result a = ..." and | > then "from_val :: Val result a -> Maybe a". | | Aha! Why didn't I think of "plain" old MPTC+fundep? For some reason | type families feel a lot more fun. Turns out you can write 'instance | Typecheck (SomeMonad result) result' and instead of complaining about | a duplicate symbol it unifies 'result', exactly like I wanted. I'm interested in situations where you think fundeps work and type families don't. Reason: no one knows how to make fundeps work cleanly with local type constraints (such as GADTs). If you think you have such as case, do send me a test case. Thanks Simon