Remora is a higher-order functional array programming language based on
the rank-polymorphic computational model originally developed by
Iverson for APL.
Unlike APL, Remora has a dependent type system that
captures array shapes for use by the parallelizing compiler.
Given that the type system is decidably checkable and inferrable,
it inevitably must have limits on its expressiveness.
In this paper, we extend Remora's type system by allowing programmers
to refine array shapes with extra constraints,
which are then checked by an SMT solver.
We develop the shape-refinement type extensions for Remora;
evaluate its utility for refining the types of standard computational kernels,
such as convolution, as well as total applications,
such as the YOLO vision application;
and prove its type soundness.