A conversation with Ulf Norell (the first implementor of Agda) led to
#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 heisenbug): Replying to [comment:48 goldfire]: this interesting thought: We may not want injectivity -- we may want a weaker property, which I'll term "head-injectivity".
So when our goal is to make progress from the target expression towards the source expression, what hinders us to follow Omega and use narrowing to obtain the head? Tim Sheard has a nice 2006 paper on how to do it. It is really powerful and we could insist that exactly one solution exists. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/6018#comment:56 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler