  We consider type inference for guarded recursive data types (GRDTs) -- a
recent generalization of algebraic data types. We reduce type inference for
GRDTs to unification under a mixed prefix. Thus, we obtain efficient type
inference. Inference is incomplete because the set of type constraints allowed
to appear in the type system is only a subset of those type constraints
generated by type inference. Hence, inference only succeeds if the program is
sufficiently type annotated. We present refined procedures to infer types
incrementally and to assist the user in identifying which pieces of type
information are missing. Additionally, we introduce procedures to test if a
type is not principal and to find a principal type if one exists.
