Force key generation in PT2CT

[cmlsharp]

Summary of our email correspondence on this subject:

Currently, keys are generated on-demand which means that if it is never strictly necessary to generate a key, we don't. This has some unfortunate side effects

double_ = lam $ \x -> x +: x
(doubleCt, keys, hints) <- runKeysHints 5.0 $ pt2ct @... double_
print keys -- []

This can even effect the pretty-printed output when used with ERW:

type PT = PNoiseCyc PNZ CT F4 (Zq 7)
double_ :: _ => expr e (_ -> _ -> PT)
double_ = lam $ \x -> lam $ \y -> var x +: var y

main = evalErrorRates 5.0 $ do
  f <- pt2ct @M'Map @Zqs @TrivGad @Int64 double_
  f' <- readerToAccumulator $ writeErrorRates @Int64 @_ @(Writer _) f
  putStrLnIO $ pprint f'

prints

(pure (\v0 -> (pure (\v1 -> ((bind ((bind (pure (\v2 -> (pure (\v3 -> (pure ((add v2) v3))))))) (bind (pure v0)))) (bind (pure v0)))))))

Note the lack of error rate logging. Since no keys are ever generated, ERW can't generate any error rate logging code so it doesn't appear in the pretty-printed output. After these changes in this PR, the same program outputs the expected

(pure (\v0 -> ((bind ((bind (pure (\v1 -> (pure (\v2 -> (((((\v2 -> (\v3 -> ((\v4 -> (\v5 -> (\v6 -> ((v4 v6) (v5 v6))))) (((\v4 -> (\v5 -> (\v6 -> (v4 (v5 v6))))) v2) v3)))) fmap) (\v2 -> (\v3 -> v2))) (\v2 -> (tell ((cons ((pair add_Q268440577) (errorRate <KEY> v2))) nil)))) ((add v1) v2))))))) (bind (pure v0)))) (bind (pure v0)))))

Note that while we could move this key generation into e.g. add_/neg_ etc., this would cause a substantial increase in their instance heads (GenSKCtx constraint is required which means bringing t) into scope, etc.). It also wouldn't account for trivial examples like lam $ \x -> x.

This PR adds an external dependency on the type-list package for the Insert and Union type families. The implementations of these are pretty trivial, but it seemed silly to reinvent them.

The implementation of this PR could be made substantially simpler by pending changes to Lol (Cyc class) which would allow a GenKeys that just iterated over the m'map indices. Currently this won't work since getKey needs the full Cyc type which includes the tensor type t. This change would allow us to get rid of AccumKeyTypes entirely.

[cpeikert]

Thanks for writing this up. I'm going to let this one simmer until we have a better idea of how the updated Lol will look, and how/whether that will change things.