#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: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * resolution: => wontfix Comment: It just occurred to me that the entire premise of this ticket is wrong. I claimed: Replying to [ticket:12119 RyanGlScott]:
For the longest time, I've wanted to make a type family like this injective:
{{{#!hs type family Foo (a :: *) :: * where Foo Bar = Int Foo Baz = Char }}}
But the problem is that `Foo` is defined on //all// types of kind `*`, so the above definition is inherently non-injective.
But the "inherently non-injective" part is totally bogus! In fact, as the code below demonstrates, `Foo` can be made injective quite easily: {{{#!hs {-# LANGUAGE TypeFamilyDependencies #-} data Bar data Baz type family Foo (a :: *) = (r :: *) | r -> a where Foo Bar = Int Foo Baz = Char }}} I don't know why I believed that crazy misconception about injectivity //vis-à-vis// exhaustivity, but in any case, the entire reason why I was pursuing this feature in the first place has vanished. In light of this, I don't think it's worth adding this much extra complexity to the type family injectivity checker. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12119#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler