The type of a `data` constructor should *not* have repeated indices unless defined within the scope of `with-K`

[jamesmckinna]

See the discussion on #2504 for a specific instance.

This raises the issue to library level, given the ambient stdlib assumption of cubical-compatible/without-K.

data constructors which exploit repeated occurrences/'non-linearity' are making implicit appeal to reflexivity of (propositional) equality, and that should instead be required as an explicit witness. Specialising the constructor to supply refl as a default witness should be the preferred approach to offering a non-linear constructor. Cf. Data.Nat.Divisibility.Core #2013

[MatthewDaggitt]

I agree this is a good principle going forward. However, how many definitions fall foul of this currently? Depending on the numbers I would be weary of how big a breaking change this would be to change all the existing definitions?

[jamesmckinna]

I haven't done a survey of the relevant definitions, besides Data.Nat.Base._≤′_, which seems to fall even more easily to the corresponding refactoring as #2504 . See commit jamesmckinna@895cd32 on branch jamesmckinna/issue2519 which is ready-to-go as a PR if you think it's worthwhile.

More generally, I'd advocate piecemeal refactoring in the interests of avoiding 'large' breaking changes?

[JacquesCarette]

I agree with the design principle.

My gut feel is that this isn't likely to occur very often. But this is rather hard to search for! So piecemeal refactoring is indeed a rather reasonable way to go.

[Taneb]

Can you clarify what exactly you mean by "non-linear" here? Is it that the same variable should not appear in two different indices of a data constructor?

[jamesmckinna]

Can you clarify what exactly you mean by "non-linear" here? Is it that the same variable should not appear in two different indices of a data constructor?

Yes, exactly. I'll change the title of the issue.

In the originating PR #2504 it's actually even stronger than that, because it meant that those indices could even become parameters to the data definition.