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
#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 jstolarek): Can I get some more time before I throw in the towel? Say, until next Thursday? Simon, if you were to start working on this what parts of my implementation need to be finished? Everything up to `SynTyCon` storing a list of `Bool`s? In what form would you like my patch? A differential revision? A branch on github? Do you want my work rebased against latest HEAD? former. No more than that. Obviously, this is what we currently have for data types and what we want for injective type families. But from the OutsideIn paper my understanding was that *current* treatment of *type families* is different. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/6018#comment:92 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler