Typechanging param fails (with poor error message) when some subtype ignores the parameter

[brprice]

(This is partially a request for a two-line change, but I am not familiar enough with the package to be sure it is actually an improvement. I have written up some background and opened this as an issue as a place to discuss it.)

In the code

data Foo a = Foo (Bar a)
  deriving Generic
data Bar a = Bar
  deriving Generic

trav :: Traversal (Bar a) (Bar b) a b
trav = param @0

trav2 :: Traversal (Foo a) (Foo b) a b
trav2 = param @0

we have that trav compiles fine, but trav2 fails to compile, saying

T.hs:22:9: error:
    • Could not deduce (Data.Generics.Product.Internal.Types.HasTypesOpt
                          ChGeneric
                          'False
                          (Bar (Param 0 a))
                          (Bar (Param 0 b))
                          (Param 0 a)
                          (Param 0 b))
        arising from a use of ‘param’
      from the context: Applicative f
        bound by the type signature for:
                   trav2 :: forall a b (f :: * -> *).
                            Applicative f =>
                            (a -> f b) -> Foo a -> f (Foo b)
        at T.hs:21:1-38
    • In the expression: param @0
      In an equation for ‘trav2’: trav2 = param @0
   |
22 | trav2 = param @0

This is a rather inscrutable message, especially as intuitively trav2 is an entirely sensible (empty) traversal, and I think could be supported (see below).

I ran across this when attempting to split a commit in two: firstly a boring preparatory commit changing data T a = ... | C Int into data T a = ... | C (S a) ; data S a = Boring Int (and the knockon churn this requires); secondly adding a new feature via data S a = Boring Int | Interesting a (which can be focused on the interesting changes). Whilst the end result works fine, the intermediate state runs into the above error.

---

My understanding is that this instance is wanted due to

• Initially need HasParam 0 (Foo a) (Foo b) a b
• This requires GHasTypes ChGeneric (RepN (Foo a)) (RepN (Foo b)) (Param 0 a) (Param 0 b)
• Unfolding generics: GHasTypes ChGeneric (Rec0 (Bar (Param 0 a))) (Rec0 (Bar (Param 0 b))) (Param 0 a) (Param 0 b)
• This needs GHasTypesUsing ChGeneric (Bar (Param 0 a)) (Bar (Param 0 b)) (Param 0 a) (Param 0 b)
• and then HasTypesOpt ChGeneric (Interesting ChGeneric (Param 0 a) (Bar (Param 0 a))) (Bar (Param 0 a)) (Bar (Param 0 b)) (Param 0 a) (Param 0 b)
• this Interesting turns out to be False

I think this Interesting is to short-circuit the traversal when there are branches that cannot contain a focus, hence the only instance is for where source and target are the same type

instance HasTypesOpt ch 'False s s a b where
  typesOpt _ = pure

Certainly we do not want to defeat this optimisation by traversing that branch just to change the type Bar a into Bar b (which naively would require deconstructing the whole tree and then re-constructing with a changed parameter. However, this only affects the type level, and not the term level, so we could use a zero-cost coerce instead.

Would it be sensible to change the instance to

instance Coercible s t => HasTypesOpt ch 'False s t a b where
  typesOpt _ = pure . coerce