I have a problem with injectivity of injective type families, here it's:

> :info F
type F :: * -> *
type family F t where = r | r -> t
. . .
> f :: forall a b . (F a ~ F b) => a :~: b; f = Refl
<interactive>: error:
• Could not deduce: a ~ b
from the context: F a ~ F b

Hi!

I have a problem with injectivity of injective type families, here it's:

Why so? Shouldn't it be injective by definition?

just a wild guess here, but do you have to write

`type family F t = r | r -> t where`

, or does the way you wrote it work the same way?oh no my mistake; that's GHC dumping the definition

Already found the cause, an incomplete TypeFamilyDependencies implementation because of lack of soundness proof https://gitlab.haskell.org/ghc/ghc/-/issues/10833

oof! thanks for updating with the solution