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