Is isn't transitive

[adamgundry]

If we have Is k l and Is l m, we do not automatically have Is k m even though it holds for all concrete instances. For example:

f :: Is k A_Fold => Optic k i s t a b -> Optic A_Fold i s t a b
f = castOptic

is perfectly fine, but

f :: Is k A_Traversal => Optic k i s t a b -> Optic A_Fold i s t a b
f = castOptic

results in the following mess:

    • Overlapping instances for Is k A_Fold
        arising from a use of ‘castOptic’
      Matching instances:
        instance [overlappable] (TypeError ...) => Is k l
          -- Defined at src/Optics/Internal/Optic/Subtyping.hs:35:31
        instance Is k k
          -- Defined at src/Optics/Internal/Optic/Subtyping.hs:31:10
        instance Is A_Getter A_Fold
          -- Defined at src/Optics/Internal/Optic/Subtyping.hs:132:10
        ...plus 7 others
        (use -fprint-potential-instances to see them all)
      (The choice depends on the instantiation of ‘k’
       To pick the first instance above, use IncoherentInstances
       when compiling the other instance declarations)

I noticed this looking at the implementation of adjoin in #332, where explicit castOptic calls are needed to call toListOf on a(n optic that can be cast to a) traversal. I wonder if we can provide a bit more information to help out type inference here. General transitivity is probably infeasible (too much guessing) but if we know e.g. Is k A_Traversal it might be possible to have Is k A_Fold etc. available from superclasses?

Another question is whether this is worthwhile, given that this most likely only arises within optics itself or for users who define their own optics combinators, rather than in normal user code (which will typically have more concrete optics).

[adamgundry]

I experimented with this a bit on branch 334-is-facts, defining

class IsFacts k l => Is k l

type IsFacts k l = (IsFacts1 k l, IsFacts2 k l)

type family IsFacts1 (k :: OpticKind) (l :: OpticKind) :: Constraint where
  IsFacts1 k A_Traversal        = (Is k A_Fold, Is k A_Setter)
  ...
  IsFacts1 k l                  = ()

type family IsFacts2 (k :: OpticKind) (l :: OpticKind) :: Constraint where
  IsFacts2 An_AffineTraversal k = (Is A_Prism k, Is A_Lens k)
  IsFacts2 A_Traversal k        = Is An_AffineTraversal k
  ...
  IsFacts2 k l                  = ()

and adding IsFacts to the context of the reflexive and overlappable error instances of Is.

This "works", in that e.g. whenever we have Is k A_Traversal in the context, we have Is k A_Fold available too, so we can remove a few castOptic calls from the internals. However, it has a somewhat unfortunate effect on error messages: a case like view mapped correctly complains that A_Setter is not A_Getter, but also emits extra messages that it is not A_Fold or An_AffineFold either. As far as I can see, the only way to avoid this is to drop the overlappable error instance for Is, so that we go back to messages like Could not deduce (Is A_Setter A_Getter).

It's unfortunate that when an instance context contains a TypeError, GHC still requires the other superclass constraints to be satisfied. When used as a constraint, TypeError could in principle be interpreted as falsum and any other constraints be satisfied by ex falso quodlibet. I wonder if this is worth a GHC issue.

The reflexive case is also somewhat problematic, because either it needs IsFacts in the context, and hence the expansion of IsFacts k k shows up whenever Is k k is needed for polymorphic k, or we need to replace the Is k k instance with a family of concrete instantiations.

It may be interesting to add more things to IsFacts, e.g. Join k l ~ l. Perhaps this leads to more compelling examples.

So far I don't think the benefit (slightly more convenient handling of definitions that have Is polymorphic in one optic kind and monomorphic in another) is worth the cost (complexity, worse type errors). But there's more to think about here... see also #308.