Suppose I have a function
f : Vect m Nat -> Vect n Nat -> {auto _ : Proof m n} -> Foo m n
where
data Proof : Nat -> Nat -> Type where
Eq : Proof x x
One : Proof 1 _
I can make a Proof 1 1 as Eq or One. Thus these aren't "orthogonal". In more complicated examples, I can have recursive data constructors where I might be able to provide a proof as Constructor1 Constructor2 or Constructor3 Constructor1. Does it matter if constructors aren't orthogonal? In particular, does it hinder proof search?
Orthogonal data constructors make it simpler and clearer to implement functions. With overlapping constructors, you will be duplicating behaviour between patterns e.g.
foo : Proof x y -> ?
foo Eq = ?eq
foo One = ?one -- duplicates `foo (Eq {x = 1})`