Skip to content

Implement homogeneous equality

As observed in two papers, the primitive equality type in GHC can be made homogeneous. This is both a simplification over the status quo (heterogeneous equality) and an important step toward implementing dependent types.

This ticket is to track this change.

Step 1: Modify the type-checker to use predicates instead of types internally. This will essentially be a glorification of PredTree (renamed Pred), and a CtEvidence will now store a Pred, not a PredType.

See also https://gitlab.haskell.org/ghc/ghc/wikis/dependent-haskell/phase2, which has much discussion.

Edited by Richard Eisenberg
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information