yet another re-implementation:
. maintain explicit mapping from unspecified to specified consts (no
dependency graph, no termination check, but direct reduction of
specifications);
. more precise checking of LHS patterns -- specialized patterns
(e.g. 'a => 'a instead of general 'a => 'b) impose global
restrictions;