Depend on sop-core about generics-mrsop

[VictorCMiraldo]

We really only care about the NS and NP types. For the sake of compatibility with other libraries in the future, I think we could just import Data.SOP (NP(..)) in Generics.MRSOP.Base.NP and the same in NS.

[arianvp]

Yes. That is exactly what I wanted to suggest :)

[VictorCMiraldo]

For the sake of documenting; this does conflict with #39 !

I'm of the opinion that #39 will eventually become obsolete once they fix GHC's bug. Nevertheless,
if the 8.8 release does not fix it, I will give a shot at #39, which will break the sop-core dependency.

[VictorCMiraldo]

In the light of the new developments in #39, which didn't solve anything, I'm a go on this suggestion!

We should organize a pull request and try to close some issues together with this refactor, so we do a single major version bump (i.e., #44 and #42 )

[VictorCMiraldo]

We have decided we will not add an extra dependency for two datatypes only.

[VictorCMiraldo]

After discussing with Andres at ICFP, I was convinced it is better to depend on sop-core than to
roll my own NS and NP datatypes.

[VictorCMiraldo]

As usual; not so straight forward. I gave it a quick go at c6bd21b but then got stuck on a typeclass hell.

Data.SOP.Constraint defines the following instances for NS and NP:

instance (All (Compose Show f) xs) => Show (NS f xs) where ...
instance (All (Compose Eq f) xs) => Eq (NS f xs) where ...

Which makes sense, but are harder to thread through generics-mrsop, where
we abstracted it differently, by the means of the showHO.

[serras]

Where do the problems arise more concretely?

[VictorCMiraldo]

I'm not 100% yet; I'm trying to remove the ShowHO and EqHO typeclasses we had. I just made
them into the following constraint-synonyms:

type EqHO   f = forall x . Eq (f x)
type ShowHO f = forall x . Show (f x)

In the old Generics.MRSOP.Zippers.Deep we'd have to carry some constraint in the Ctx datatype.
I just removed the module as the shallow zippers should suffice.

I'm now trying to compile generics-mrsop-gdiff and hdiff; if I succeed on these, I'd happily drop EqHO and ShowHO and stick with the quantified constraints versions above and unify everything
with sop-core.

[VictorCMiraldo]

@serras

The process has been mainly mechanic so far; We will need to add things like
the following instance to mrsop, though.

type EqHO   f = forall x . Eq (f x)
instance (EqHO f , EqHO g) => Eq ((f :*: g) x) where
  (==) (fx :*: gx) (fy :*: gy) = fx == fy && gx == gy

[serras]

I thinl you can even abstract the EqHO type as:

type HO (c :: r -> Constraint) (f :: k -> r) = forall (x :: k). c (f x)
instance (HO Eq f, HO Eq g) => Eq ((f :*: g) x) where ...

Now you don't need a different ConstraintHO for each constraint.

[VictorCMiraldo]

That makes sense; It's just that a good amount of code already has EqHO and ShowHO spread through it.

In any way; if I understand -XQuantifiedConstraints, this shouldn't be different from our
manual handling of higher-order though our (old) EqHO.

@serras , I got some impredicative polymorphism error right here, for which I had to pull the quantified constraints out
and distribute them by hand. Not sure if this was supposed to happen or if type annotations would fix this.

[serras]

You can always define EqHO as HO Eq and keep the code the same.

Note however that -XQuantifiedConstraints sometimes asks for more than a higher-order version. In the case of something like NP, you can ask for Eq (f x) for every x in a type-level list; if you ask for forall x. Eq (f x) this requires for every x in Type.

[serras]

@serras , I got some impredicative polymorphism error right here, for which I had to pull the quantified constraints out
and distribute them by hand. Not sure if this was supposed to happen or if type annotations would fix this.

Yes, there seems to be some weird things happening when you abstract over constraints with foralls. Something they "count" as quantified constraints , and everything is fine, sometimes they are rank-n types, and then GHC starts asking for impredicative polymorphism.

I guess the best solution is what you are doing: just thread the constraints by hand.