Re: Type family equation violates injectivity?