#6018: Injective type families -------------------------------+------------------------------------------- Reporter: lunaris | Owner: simonpj Type: feature | Status: new request | Milestone: 7.10.1 Priority: normal | Version: 7.4.1 Component: Compiler | Keywords: TypeFamilies, Injective Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: #4259 None/Unknown | Test Case: | Blocking: | -------------------------------+------------------------------------------- Comment (by jstolarek): I spent some time recently thinking about this one. It is not clear to me what should happen when we know that a type family `F` is injective. It would certainly allow us to infer from `(F a ~ F b)` that `a ~ b` (modulo corner cases). So instead of first reducing injective type family application and then working on the result we could instead reason about type family's arguments. We could even invert type families. Is there anything else we could reason about with injective type families? The discussion here is only about open type families (obviously, closed type families were not implemented two years ago). I guess that now this change would affect both open and closed type families? Replying to [comment:2 simonpj]:

Some functions might be injective in one argument but not another. For example: {{{ F a b ~ F c d ===> a ~ c but not b ~ d }}} That is not true according to the mathematical definition of injectivity (as stated in [comment:29 comment 29]). Unless we want to introduce definition of type families injective only in some of the arguments, [http://haskell.1045720.n5.nabble.com/Injective-type-families- tp3385084p3385684.html as proposed by Iavor].

-- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/6018#comment:32 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler