GitLab

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.