#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 simonpj): (GHC does, in effect, use narrowing, I believe.) Let's stand back a bit. What are we trying to achieve. Here is the Number 1 Goal: if the type inference engine is trying to prove `F a ~ F beta`, where `a` is a skolem constant and `beta` is a unification variable, is it justified in fixing `beta := a`? If `F` is not injective the answer is "no". If it's injective, the answer is "yes". We have multiple examples of the need for this. More generally, our goal is to use injectivity to guide the decision about what type a unification varaible stands for. Injectivity also allows other such opportunities, beyond the Number 1 Goal above. Suppose `F` is injective, and we have {{{ F Int = True }}} Then if we have `F beta ~ True` we can deduce `beta := Int`. Richard raises further possiblities: possibly-partial information about the result might allow us to deduce possibly-partial information about the arguments. That is the stuff about head-injectivity and it seems to be potentially very complicated. Take a closed type family. If I tell you something (but perhaps not everything) about the result, perhaps you can tell me something (but perhaps not everything) about the argument. I don't know how clever you might be here, or how to declare the cleverness in an "injectivity signature" for open families. But we have no actual use-caes for anything except Number 1 Goal, for equalities of form `F t1 ~ F t2`. It seems that equalities of form `F t1 ~ some-type` offer potential opportunities, but I don't see a sweet spot. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/6018#comment:57 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler