injectivity of injective type families - Haskell

Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

Yuriy Pitomets


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

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

Matt Peddie

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?

Matt Peddie

oh no my mistake; that's GHC dumping the definition

Yuriy Pitomets

Already found the cause, an incomplete TypeFamilyDependencies implementation because of lack of soundness proof

Matt Peddie

oof! thanks for updating with the solution