  We introduce a type system for the Quipper language designed to derive upper
bounds on the size of the circuits produced by the typed program. This size can
be measured according to various metrics, including width, depth and gate
count, but also variations thereof obtained by considering only some wire types
or some gate kinds. The key ingredients for achieving this level of flexibility
are effects and refinement types, both relying on indices, that is, generic
arithmetic expressions whose operators are interpreted differently depending on
the target metric. The approach is shown to be correct through logical
predicates, under reasonable assumptions about the chosen resource metric. This
approach is empirically evaluated through the QuRA tool, showing that, in many
cases, inferring tight bounds is possible in a fully automatic way.
