#12119: Can't create injective type family equation with TypeError as the RHS -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: feature request | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: wontfix | CustomTypeErrors, TypeFamilies, | InjectiveFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by AntC): The injectivity annotation is a promise that all your equations are injective. Then consider the return ''type'' of `ToDim 5` compared to `ToDim 6` (if you put a `TypeError` equation): they're the same type. Then that equation is not injective. Specifically, `ShowType n` is not injective: [https://downloads.haskell.org/~ghc/latest/docs/html/libraries/base-4.12.0.0/... /GHC-TypeLits.html#AppendSymbol it's an existentially-quantified data constructor, promoted to a datakind]. If you omit the `TypeError` equation, there's an implicit `ToDim n = ToDim n` added at the end. That is injective. Possibly you could put some other error-handling logic, that preserves plain `n` on the rhs, then that would be injective. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12119#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler