[GHC] #6018: Injective type families

[GHC]

#6018: Injective type families
-------------------------------------+-------------------------------------
        Reporter:  lunaris           |                   Owner:  jstolarek
            Type:  feature request   |                  Status:  new
        Priority:  normal            |               Milestone:  7.12.1
       Component:  Compiler          |                 Version:  7.4.1
      Resolution:                    |                Keywords:
Operating System:  Unknown/Multiple  |  TypeFamilies, Injective
 Type of failure:  None/Unknown      |            Architecture:
      Blocked By:                    |  Unknown/Multiple
 Related Tickets:  #4259             |               Test Case:
                                     |                Blocking:
                                     |  Differential Revisions:  Phab:D202
-------------------------------------+-------------------------------------

Comment (by jstolarek):

 Replying to [comment:103 jberryman]:
 > I've only had use for better type inference with (conceptually) closed,
 recursive type families
 Calling type families from an injective type family will not be allowed
 (including recursion). The reason is that I don't see a way of verifying
 injectivity when type families are involved.

 > What I think I want is something like proposal C from the wiki
 At the moment I am implementing proposals A and B. C is something to think
 about in the future, as it is not trivial.

 > And as a naive user I want injectivity to be inferred for closed type
 families, and don't find the arguments against it in the wiki convincing.
 Yes, I suppose that focus of the wiki discussion is a bit off. I think we
 could infer injectivity of type A for closed type families. But I don't
 think we should try to infer injectivity of type B because the algorithm
 is exponential - see [comment:64 comment 64]. That's the major reason for
 doing this. (Numbers in that comment were computed for type C injectivity,
 but type B is also exponential.)

 {{{#!hs
 -- | The algebraic normal form 'Exponent' @abc@ distributed over the
 single
 -- base variable @x at .
 type family abc :=>-> x
 -- | x¹ = x
 type instance () :=>-> x = x
 -- | x⁽ᵃᵇ⁾ = (xᵇ)ᵃ
 type instance (a,bs) :=>-> x = a -> bs :=>-> x
 }}}

 I don't think `:=>->` type family is injective: both `() :=>-> (Int ->
 Int)` and `(Int,()) :=>-> Int` reduce to `Int -> Int`.

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