## Incremental `tcCheckSatisfiability` API

The pattern-match checker makes use of the function `tcCheckSatisfiability :: Bag EvVar -> TcM Bool`

(henceforth `tcCS`

) offered by the type-checker to solve type constraints. Over the course of a pattern-match checking session, such a `Bag EvVar`

is accumulated and incrementally checked after each addition. As #17836 (closed) shows in a rather painful way, that scales quadratically, because the type-checker chews through the same type constraints over and over again.

But look at how the pattern-match checker uses `tcCS`

:

```
-- | Add some extra type constraints to the 'TyState'; return 'Nothing' if we
-- find a contradiction (e.g. @Int ~ Bool@).
tyOracle :: TyState -> Bag PredType -> DsM (Maybe TyState)
tyOracle (TySt inert) cts
= do { evs <- traverse nameTyCt cts
; let new_inert = inert `unionBags` evs
; ... <- initTcDsForSolver $ tcCheckSatisfiability new_inert
; ... }
```

The `inert`

set is a `Bag EvVar`

for which *we already know they are compatible with each other*, as they were checked by `tcCS`

in a previous call. Only `cts :: Bag PredType`

are unchecked. And as far as the pattern-match checker is concerned, the type of `inert`

is completely opaque, so the API to `tcCS`

could very well be

```
tcCheckSatisfiability :: TcInert -> Bag EvVar -> TcM (Maybe TcInert)
-- | Add some extra type constraints to the 'TyState'; return 'Nothing' if we
-- find a contradiction (e.g. @Int ~ Bool@).
tyOracle :: TyState -> Bag PredType -> DsM (Maybe TyState)
tyOracle (TySt inert) cts
= do { evs <- traverse nameTyCt cts
; ...mb_new_inert... <- initTcDsForSolver $ tcCheckSatisfiability inert evs
; ... }
```

I'm sure there already is something like `TcInert`

in the type-checker. Looking at the implementation of `tcCS`

, that might be the unused `EvBindMap`

, but I'm not sure. Or is it the `InertCans`

in `getInertCans`

/`setInertCans`

? CC @rae, @RyanGlScott, @simonpj

This blocks #17836 (closed) and would probably lead to quite a few (possibly rather drastic) metric decreases in other cases.