Straightened out implicit coercions for indexed types