  A method for selecting solution constructors in narrowing is presented. The
method is based on a sort discipline that describes regular sets of ground
constructor terms as sorts. It is extended to cope with regular sets of ground
substitutions, thus allowing different sorts to be computed for terms with
different variable bindings. An algorithm for computing signatures of
equationally defined functions is given that allows potentially infinite
overloading. Applications to formal program development are sketched.
