Idea is simple: we need same constraints on "implementation" and "argument deduction. Syntax may change.