check' TypedTh checking Braty in parallel with Kernel breaks the Store

[acl-cqc]

  Braty -> do
    -- but the computation in it could be either Brat or Kern
    brat <- catchErr $ check t ((), ())
    kern <- catchErr $ let ?my = Kerny in check t ((), ())

tries both Kern and Braty and picks whichever succeeds. But even a failing check could define things in the Store that then breaks the second attempt. (A succeeding check could also define things that makes the second fail when it might also have succeeded, we're not sure if such cases exist.)

So, either we need some kind of transaction (commit/rollback), or some reliable way to tell whether the contents of the TypedTh is Brat or Kernel.

However, we're not sure we have any coverage of TypedTh at all (just there for completeness)...