Decidability of Type-Checking in the Calculus of Algebraic Constructions with Size Annotations