Skip to content

WIP: Add evidence for type family injectivity

mniip requested to merge mniip/ghc:injective into master

This fixes #10833 , namely implications of the form F a ~ F b => a ~ b. There was a discrepancy between the solver believing we can't use SelCo for tyfam tycons, and the core linter actually allowing them.

This is a user-facing change: more programs are accepted. TODO: ghc-proposals.

Addressing the case for F a ~ Y => a ~ X would require significantly more work.

This was the result of the GHC workshop.

Edited by mniip

Merge request reports