#6018: Injective type families -------------------------------------+------------------------------------- Reporter: lunaris | Owner: jstolarek Type: feature | Status: new request | Milestone: 7.10.1 Priority: normal | Version: 7.4.1 Component: Compiler | Keywords: TypeFamilies, Resolution: | Injective Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: #4259 Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by goldfire): A conversation with Ulf Norell (the first implementor of Agda) led to this interesting thought: We may not want injectivity -- we may want a weaker property, which I'll term "head-injectivity". The equations defining a head-injective function all have RHSs with different heads. What appears below the heads does not matter. Here is an example: {{{#!hs type family F a where F (Just x) = True F Nothing = False }}} This function is ''not'' injective: `F (Just 1) ~ F (Just 2)`. Yet, it is head-injective. If the type-inferencer knows that `F x ~ True`, it can then refine `x ~ Just y` for some fresh unification variable `y`. This improvement may be enough to make further progress. Of course, injectivity does not imply head-injectivity. Consider {{{#!hs type family G a where G True = Just 1 G False = Just 2 }}} This function is injective but not head-injective. So, implementing only head-injectivity will miss this case. But, perhaps we can refine the notion of head-injectivity simply to mean that the RHSs don't unify. The reason I'm bringing this up is that head-injectivity is, as I understand it, implemented in Agda and used during type inference. It intrigues me to think that we can make progress in the case of `F`, a non- injective function. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/6018#comment:48 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler