#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: Phab:D202 | -------------------------------------+------------------------------------- Comment (by simonpj): Re comment:89 and comment:90 I'm struggling with limited personal bandwidth, and daunted by the challenge of giving a tutorial about the type inference engine, which is one of the most complex parts of GHC. Let me make this offer. If you do the rest, I'll do the bit in the type inference engine that exploits injectivity. It won't take long, and then you can see. Decomposition in brief. If you want `Maybe a ~ Maybe b` then it's enough to prove `a ~ b`. From a proof of the latter we can get a proof of the former. No more than that. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/6018#comment:91 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler