[GHC] #6018: Injective type families

[GHC]

#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):

 I've made a major update to the wiki page. Here are a few things worth
 pointing out:

 In [wiki:InjectiveTypeFamilies#Proposedsyntax this section] I've listed
 all the syntax proposals made so far. I've also
 [http://www.haskell.org/pipermail/haskell-cafe/2014-September/116065.html
 mailed Haskell-cafe] so we can get some feedback from the community.

 I christened various flavours of injectivity as A, B and C :-) -- see
 [wiki:InjectiveTypeFamilies#Formsofinjectivity this section]. I will refer
 to them as such in the rest of this comment.

 I mailed Conal Elliot and he says he does not remember what was his use
 case for type families injective in only one argument. This means we only
 have use cases of the form A shown by Simon. Given that, I believe that it
 is best if we limit ourselves to implementing A. We can revise this design
 later if someone demonstrates compelling examples of B or C.

 I have outlined my idea for the algorithm that would verify users
 injectivity declarations in
 [wiki:InjectiveTypeFamilies#Implementationoutline this section]. Simon,
 please tell me if there are any misconceptions about how GHC's type
 inference works.

 After some thinking I am against inferring injectivity for closed type
 families - see my arguments in
 [wiki:InjectiveTypeFamilies#Inferringinjectivity this section].

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