Skip to content

GitLab

Open
Created by Richard Eisenberg@raeDeveloper

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