Refactor range constraints in `ArithmeticCircuit`

[vlasin]

In parallel with #249, we must refactor the acRange field in the ArithmeticCircuit type. Instead of having a map from variables to their upper bound value, it makes sense to have a number of predefined sets (possibly of different dimensions):

$$ T_1, \dots, T_m $$

A constraint that we will support has a form

$$ (x1, \dots, x{k(j)}) \in T_j, \quad T_j \in {T_1, \dots, T_m}. $$

It makes sense for the sets $T_j$ to parameterise a circuit on a type level, so that adding an unsupported constraint to a circuit will be caught at compile time.

[TurtlePU]

If $T_j$ parameterize a circuit on a type level, this should be visible in a MonadCircuit API which is accessible via Symbolic typeclass, so this leaks into Symbolic API. Then this will lead to the same Sig problem we had before, this time with lookups which generic context c should support.

If this is okay, then sure, why not. (This might really be okay because the list of possible lookups is infinitely smaller than the list of possible instances of classes for Symbolic datatypes)

This can be done in a plethora of ways.

1. One is via HasLookup marker trait:

   
   -- | New definitions
   data Lookup = Range Natural | ...
   class HasLookup (l :: Lookup) p

-- | Current API updates

class MonadCircuit var a m | m -> a, m -> var where -- | Other methods are omitted for clarity newRanged :: HasLookup (Range n) m => Witness var a -> m var

class Symbolic c where -- | symbolicF is omitted for clarity fromCircuit :: (forall var a m. (MonadCircuit var a m, forall l. HasLookup l c => HasLookup l m) => f var -> m (g var) ) -> c f -> c g -- ^ Note that this way we have to specify which lookups context c Has. -- This will soon lead to the same problem we had with Sigs.

data ArithmeticCircuit (ls :: [Lookup]) a i o = -- ... -- instance In l ls => HasLookup l (ArithmeticCircuit ls a i) instance (In l ls, o ~ U1) => HasLookup l (MonadState (ArithmeticCircuit ls a i o)) -- ^ In l ls is a type family which compiles iff l is in ls

instance HasLookup l (Interpreter a) instance HasLookup l (Witnesses a) -- ^ lookups are not checked in Interpreter context

  * We can also add a `HasLookups` helper type family for clarity:
```haskell
type family HasLookups (ls :: [Lookup]) p where
  HasLookups '[] p = ()
  HasLookups (l ': ls) p = (HasLookup l p, HasLookups ls p)

2. The other is via adding the (ls :: [Lookup]) type-level parameter both to Symbolic and to MonadCircuit class declarations.

[TurtlePU]

Or maybe it shouldn't be visible in a MonadCircuit and we make the types in MonadCircuit permissible (leave them as-is), but we throw an error during circuit compilation if some range constraint is not allowed by the user-specified list of allowed lookups.

[vlasin]

Hmm, but structured I/O does not leak to Symbolic... I thought it was a similar kind of situation. Currently, the inputs and outputs of the circuit are type parameters. I am thinking about adding the type of allowed constraints as another parameter, essentially.