Type family equation violates injectivity?