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.