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?
Was it naive of me to expect this to work?
Is it not possible for equality computation rules to dispatch on arguments that bind variables? Is there a theoretical reason for that?