The unsafeCoerce can be made nicer, but I think that calculating proofs is justified. (IMHO INCOHERENT instances are about as bad as unsafeCoerce - you have to justify why it's fine to pick either).

Eh, it looks like there are weird test failures anyway.

I fixed test failures and made only one instance incoherent.

The incoherence seems fine here as there really is only one possible dictionary (modulo bottoms).

I'm less clear about the runtime performance trade-off. Will this all optimize away for nontrivial concrete index lists? I guess it might, even though appendIndices is recursive, because it is polymorphic recursion through a typeclass. And if so, there's no unsafeCoerce to gum up the inliner (EDIT: although of course in the concrete case the unsafeCoerce would be between equal types anyway, so hopefully it disappears regardless?). We could use Tagged instead of a proxy argument to make appendIndices fractionally cheaper if it does end up doing runtime work?

What about type-inference/errors, especially in the case of index-polymorphic code? Of course AppendIndices will show up in inferred types, e.g.:

*Optics.Core> :t (%)
(%)
  :: (Is k (Join k l), Is l (Join k l),
      AppendIndices is js (Append is js)) =>
     Optic k is s t u v
     -> Optic l js u v a b -> Optic (Join k l) (Append is js) s t a b

although we could make this a bit more compact by dropping the third parameter from AppendIndices, since it is entirely determined by the first two anyway.

I'm less clear about the runtime performance trade-off. Will this all optimize away for nontrivial concrete index lists?

According to my experiments it does. I modified tests so it's also checked there.

We could use Tagged instead of a proxy argument to make appendIndices fractionally cheaper if it does end up doing runtime work?

I modified it to use Proxy# instead.

What about type-inference/errors, especially in the case of index-polymorphic code?

I removed the third argument from the class, the signature looks a bit better now.

λ> :t (%)
(%)
  :: (Is k (Join k l), Is l (Join k l), AppendIndices is js) =>
     Optic k is s t u v
     -> Optic l js u v a b -> Optic (Join k l) (Append is js) s t a b

@adamgundry ping

Though I'm not 100% sure if it's worth it.

It looks like it's just going to require putting corresponding AppendIndices to the context whenever Append is used with polymorphic indices, though this ought to be internal detail.

We could use Tagged instead of a proxy argument to make appendIndices fractionally cheaper if it does end up doing runtime work?

I modified it to use Proxy# instead.

This is a point on which I'm somewhat hazy, but I think Proxy# x -> a requires a function call (albeit to a function whose arguments occupy zero bits), whereas Tagged x a is genuinely represented as a at compile-time? I doubt the difference really matters though.

Though I'm not 100% sure if it's worth it.

It looks like it's just going to require putting corresponding AppendIndices to the context whenever Append is used with polymorphic indices, though this ought to be internal detail.

Yes, I'm on the fence with this one too. The extra constraint will probably be solved automatically in most user code (which will have concrete indices), but it will still potentially show up in error messages and the like. And it does potentially incur some runtime work to get away from an unsafeCoerce that is mostly harmless AFAICS. Or are there more compelling reasons for dropping the unsafeCoerce that I'm missing?

After more consideration let's leave it.