WIP: Add evidence for type family injectivity
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.