#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 sheaf): What about the following: {{{#!hs data Dim = D2 | D3 | D4 type family ToDim (n :: Nat) = d | d -> n where ToDim 2 = D2 ToDim 3 = D3 ToDim 4 = D4 ToDim n = TypeError ( Text "Error: dimension must be 2, 3 or 4 (given: " :<>: ShowType n :<>: Text ")" ) }}} This seems useful to me, as it allows one to switch easily between two different representations of dimension (which have different uses: with Nats I can do arithmetic, but the explicit enum is more convenient with singletons for instance). I feel like the injectivity annotation should be allowed in this case (but I am not aware of any of the theory which backs injective type families). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12119#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler