constrained-generators: Split up TheKnot

[MaximilianAlgehed]

Some ideas for what we need to do to be able to do this, these will hopefully also simplify a lot of other code:

• Make the boolean insteance non-generic?
• Split TypeSpec, combineSpec, and genFromTypeSpec into three different classes from HasSpec - this might enable us to move generation downstream of everything else
• Cardinality being in terms of integer causes dependency on all the NumSpec stuff
• Using DerivingVia because we've split out TypeSpec might mean we can move the generics out of default implementations - thus breaking that dependency too (c.f. below, we'll need some better trick than this)

[MaximilianAlgehed]

One issue I should have seen coming with this plan but I only realized now after not being able to look away for a while is the fact that Coercible doesn't play as nicely as you'd like with Specification. This makes the DerivingVia plan impractical if not downright impossible. The basic problem is that you can't make GHC accept code like this:

newtype SomeNewtype a = SomeNewtype a

force :: Coercible (TypeSpec (SomeNewtype a)) (TypeSpec a) => Specification (SomeNewtype a) -> Specification a
force = coerce

even though it should be safe. The problem is that GHC hasn't inferred what I believe is the key instance for Coercible that you'd need:

instance Coercible a b, Coercible (TypeSpec a) (TypeSpec b) => Coercible (Specification a) (Specification b)

Because this would be wildly unsafe in general.

[MaximilianAlgehed]

Observations about the code-base right now:

• Logic shouldn't need Syntax

• Logic really depends on HasSpec
  (but not generation!)

• Ctx, Logic, and propagateSpec belong together as the "propagation machinery"

• Possibly we can split some of the function symbol machinery out of Base
  by not relying so much on AppRequires and being a bit more careful

• It's not impossible that we can do SpecificationRaw c a with Specification = SpecificationRaw HasSpec to
  get a "dependency injection" style solution to making at least some specification manipulation independent
  of HasSpec. The same goes for Term and Pred.

• The pretty-printing stuff can be split out of Constrained.Base

• Plan of attack:

  • Try to do the dependency injection inline
  • Minor function symbol stuff in one module
  • Specification, Pred, and Term (raw versions) in one module
    • Pred needs Forallable, need to inject this too
  • Logic stuff in one module (dependency injection here too)
    • Downstream of Specification, Pred, Term module