Efficiently ordering typed programs
Two remarks first:


I have used the "randomly generate terms and check that they are well-typed" approach (you mention that "untyped" terms are generated, you can also randomly generate terms in a Church-style grammar with explicit type annotations) and it worked very well in practice, it revealed all the bugs there was to find on this particular part of the project. For practical purposes I would recommend trying this first. (On the other hand, the generator was aware of scoping rules -- it maintained a set of currently bound variables for top-down generation, this is easy to implement.)
The choice of order depends a lot on the application you have in mind: two distinct applications will require different orders. For example, people that work on type-directed program synthesis are not usually interested in enumerating equivalent programs, so they will make simplification rules such as assuming that "any term of type A -> B can be chosen to start with a lambda-abstraction" -- in your framework, ordering lambda-terms before all terms at this type. This order is very bad for compiler testing: if you only generate programs that are in normal form, you are unlikely to exercise much of your optimization strategies or runtime semantics. So I believe that assuming an order to abstract away from the intended usage is not a good modeling choice: its choice is tightly coupled with the intended usage, and I would rather reason about the usage than the corresponding order.


Now for some references.

For typed-term generation for testing purposes, you may be interested in "Making random judgments: Automatically generating well-typed terms from the definition of a type-system" by Burke Fetscher, Koen Claessen, Michał Pałka, John Hughes, and Robert Bruce Findler, 2015.


  This paper presents a generic method for randomly generating well-
  typed expressions. It starts from a specification of a typing judgment in PLT Re-
  dex and uses a specialized solver that employs randomness to find many different
  valid derivations of the judgment form.
  Our motivation for building these random terms is to more effectively falsify
  conjectures as part of the tool-support for semantics models specified in Redex.
  Accordingly, we evaluate the generator against the other available methods for
  Redex, as well as the best available custom well-typed term generator. Our results
  show that our new generator is much more effective than generation techniques
  that do not explicitly take types into account and is competitive with generation
  techniques that do, even though they are specialized to particular type-systems
  and ours is not.


For typed term enumeration for program synthesis, two recent works that I know are Example-Directed Synthesis: A Type-Theoretic Interpretation by  Jonathan Frankle, Peter-Michael Osera, David Walker, and Steve Zdancewic, 2016, and Program Synthesis from Polymorphic Refinement Types by Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama, 2016. Note that both works use refinement types as a way to encode more desired properties of the searched program -- such as a testsuite that it should pass. These refinements often constrain the search space substantially more than just types, but they are also harder to invert -- interleave with search.