Skip to content

PredType for type constraints in the pattern match checker instead EvVar

Sebastian Graf requested to merge wip/pmcheck-predtype into master

Using EvVars for capturing type constraints implied side-effects in DsM when we just wanted to construct type constraints.

But giving names to type constraints is only necessary when passing Givens to the type checker, of which the majority of the pattern match checker should be unaware.

Thus, we simply generate newtype TyCt = TyCt PredType, which are nicely stateless. But at the same time this means we have to allocate EvVars when we want to query the type oracle! So we keep the type oracle state as newtype TyState = TySt (Bag EvVar), which nicely makes a distinction between new, unchecked TyCts and the inert set in TyState.

Edited by Sebastian Graf

Merge request reports