#4259: Relax restrictions on type family instance overlap ----------------------------------------+----------------------------------- Reporter: lilac | Owner: Type: feature request | Status: new Priority: normal | Milestone: 7.8.1 Component: Compiler (Type checker) | Version: 6.12.1 Keywords: | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: Unknown | Testcase: Blockedby: | Blocking: Related: | ----------------------------------------+----------------------------------- Comment(by carter): Replying to [comment:23 goldfire]:

It has also become clear that the ideas leading to this thread have a more general setting than just allowing for relaxed overlap restrictions. For example, given a type family for {{{And}}}, we may want GHC to be able to simplify {{{And x y ~ True}}} to {{{(x ~ True, y ~ True)}}}... but this is certainly not straightforward type family simplification. I'm still not quite sure what the solution is, but my thought is that simply relaxed restrictions on overlap will be 1) hard to do right and 2) not quite enough power anyway.

being able to "prove" (And x y) ~ True ---> (x~ True,y~True), and other things like it, that seems like it'd be a generalization of whats needed for Injective type families, right? -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4259#comment:26 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler