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