dispatching on arguments that bind variables

[mikeshulman]

Was it naive of me to expect this to work?

require eq ;;
rule foo (A type) ({x:A} B type) type ;;
rule bar (C type) type ;;
rule foo_bar (A type) ({x:A} B type) :
  foo A ({x:A} bar B{x}) ≡ foo A B ;;
eq.add_rule foo_bar ;;

Runtime error: uncaught exception ML.EqualityCheckerException
  "cannot make a pattern from a bound type metavariable"

Is it not possible for equality computation rules to dispatch on arguments that bind variables? Is there a theoretical reason for that?