As a general rule of thumb, shallow embedding is best suited for applications that use the solver to search for values processed by a program, as is typical for program verification and angelic execution.
Deep embedding is the best choice if you are doing program synthesis and searching for (values that represent) code.
Shallow embedding can be a good choice for program synthesis if your application will be searching just for constants. But if you are searching for anything more complex (e.g., expressions or statements), deep embedding is the way to go.
With a shallow embedding, you have limited control of the space of programs that Rosette will search. Basically, you're limited to whatever can be encoded with Rosette's macro-based sketching constructs. These allow you to define basic search spaces and write quick prototypes, but if you want to build a tool that scales, you'll want tight control of the search space.
With a deep embedding, you have total control of the space of programs that will be searched. Essentially, you can write arbitrary Rosette / Racket functions to generate the symbolic program that represents all concrete programs to be searched. You then also have total control over the final step, which is code generation. Once Rosette returns a value (e.g., an AST) that represents a program in your deep embedding, you can process it however you want to generate code. With a shallow embedding, you are limited to using Rosette's built-in code generator.
So, to conclude, if you are doing or plan to do synthesis, use a deep embedding. For everything else (verification and angelic execution), shallow embedding will be easier and quicker.
