Refactor Ct and friends
Right now, the Ct
type contains many constructors. This ticket tracks breaking up this type into smaller ones. Candidates:
-
All constraints are born as non-canonical. So the bag of constraints in the
TcM
monad are all non-canonical. This should be its own type. -
Equality constraints are dealt with separately from others. (See details on the description of the inert set.) These should be their own types, too.
-
A work list has both canonical and non-canonical constraints. But this might be the only place we need the full sum.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information