Dependency cycles involving Solver modules

[MatthewDaggitt]

While trying to fix #392 an old problem has reared its head. Namely that importing Data.List.Properties in Data.List.Relation.Pointwise results in:

cyclic module dependency:
  Data.List.Relation.Pointwise
  Data.List.Properties
  Algebra.Monoid-solver
  Data.List.Relation.Equality.DecPropositional
  Data.List.Relation.Equality.DecSetoid
  Data.List.Relation.Equality.Setoid
  Data.List.Relation.Pointwise

Similar dependency cycles have cropped up before for Solvers for other data types (Nat and Vec I think). This one is particularly nasty as we definitely don't want to have to reprove many of the pointwise list properties that are immediately inferrable from the same property holding with propositional equality.

In my opinion all solvers should be moved out of Data.X.Properties (as they're definitely not a "property") and into their own module. Perhaps Data.X.Solver? If we didn't have to worry about backwards compatibility, I would suggest moving both Solver and Reasoning modules to Data.X.Reasoning but the Reasoning modules are so widely used that it would probably cause chaos.

Thoughts?

[JacquesCarette]

I like Data.X.Solver.

But I don't see how this would fix the current problem -- isn't Algebra.Monoid-solver already in its own module? The problem seems to be that Algebra.Monoid-solver uses Data.List.Relation.Equality.DecPropositional? The other possibility is to consider Data.List so basic that many of its properties (perhaps split off in Data.List.Properties.Core) should be proved by hand rather than through the monoid solver.

[MatthewDaggitt]

But I don't see how this would fix the current problem -- isn't Algebra.Monoid-solver already in its own module?

The problem is that we use Algebra.Monoid-solver in Data.List.Properties to define 'list-solver', a special solver over _++_. This solver is never actually used in Data.List.Properties. If it was moved then Data.List.Properties wouldn't depend on Algebra.Monoid-solver and hence the cycle would be broken.

The other possibility is to consider Data.List so basic that many of its properties (perhaps split off in Data.List.Properties.Core) should be proved by hand rather than through the monoid solver.

Hence this wouldn't fix the problem.