Changes between Version 23 and Version 24 of InjectiveTypeFamilies


Ignore:
Timestamp:
Sep 3, 2015 4:45:13 AM (4 years ago)
Author:
jstolarek
Comment:

Rewrite of the wiki page after the merge of ITF branch into master

Legend:

Unmodified
Added
Removed
Modified
  • InjectiveTypeFamilies

    v23 v24  
    11= Injective type families
    22
    3 This page summarizes the design behind injective type families (#6018). For the latest information about implementation progress see [[https://phabricator.haskell.org/D202|D202]]. ETA: based on current progress I estimate that this should be completed around March 2015. This means injective type families will be available in GHC 7.12.
    4 
    5 Person responsible for this page and the implementation: Jan Stolarek (just so
    6 you now who is meant by "I").
    7 
    8 My current implementation is located on GitHub:
    9 
    10   * https://github.com/jstolarek/ghc/tree/T6018-injective-type-families
    11   * https://github.com/jstolarek/haddock/tree/T6018-injective-type-families
    12 
    13 Note that you need to update the haddock submodule as well. Since it's a work in progress things might be broken. Also, I tend to do upstream rebases with these branches so beware when using `git pull`.
     3This page summarizes the design of injective type families (#6018).
     4Implementation discussion and progress was recorded in
     5[[https://phabricator.haskell.org/D202|Phab D202]].
     6
     7As of September 2015 injective type families are merged into HEAD and will be
     8available in the next stable GHC release (8.0).
     9
     10Person responsible for this page is Jan Stolarek (just so you now who is meant
     11by "I").  I am also responsible for most of the implementation.  Simon Peyton
     12Jones and Richard Eisenberg participated in the development of theory behind
     13injective type families, so whenever I say "we" I mean the three of us.  For
     14full discussion of injective type families see Haskell Symposium 2015 paper
     15"Injective type families for Haskell" (henceforth referred to as the
     16"injectivity paper").
    1417
    1518== Forms of injectivity
    1619
    1720The idea behind #6018 is to allow users to declare that a type family is
    18 injective. So far we have identified these forms of injectivity:
     21injective.  We have identified three forms of injectivity:
    1922
    2023  A. Injectivity in all the arguments, where knowing the result (right-hand
     
    5356{{{#!hs
    5457type family Plus a b where
    55      Plus Z      n = n
    56      Plus (S m ) n = S (Plus n m)
    57 }}}
    58 
    59   Here knowing the RHS and any single argument uniquely determines the
    60   remaining argument.
     58     Plus Z     n = n
     59     Plus (S m) n = S (Plus n m)
     60}}}
     61
     62  Here knowing the RHS and the first argument uniquely determines the remaining
     63  argument.
    6164
    6265{{{#!hs
     
    7073  about `a` or `b`.
    7174
    72 
    7375In the following text I will refer to these three forms of injectivity as A, B
    7476and C.
    7577
    76 '''Note that at the moment we only have practical use cases for injectivity of
    77 form A. Because of that I propose that we implement only this form of injectivity.'''
    78 We can implement B and C when somebody comes up with compelling use cases.
     78Currently GHC implements injectivity of type B (and therefore of type A as well,
     79since A is a subset of B).
    7980
    8081== Proposed syntax
    8182
    82 Two important things to consider when deciding on a concrete syntax are:
    83 
    84   * '''Backwards compatibility''': at the moment no decision has been made on
    85     whether injectivity will become a part of existing `TypeFamilies` extension
    86     or if we create a new `InjectiveTypeFamilies` extension that implies
    87     `TypeFamilies`. If we choose the former then we need to come up with syntax
    88     that is backwards compatible. (Perhaps this is the other way around: if we
    89     end up having backwards incompatible syntax then we must create a new
    90     language extension).
    91 
    92   * '''Future extensibility''': if we only implement A we still want to be able
    93     to add B and C in the future without breaking A.
    94 
    95 We decided to use syntax similar to functional dependencies.  The injectivity
    96 declaration begins with `|` following type family declaration head.  `|` is
    97 followed by a list of comma-separated injectivity conditions. Each injectivity
    98 condition has the form:
    99 
    100 {{{#!hs
    101 A -> B
    102 }}}
    103 
    104 where `A` and `B` are non-empty lists of type variables declared in type family
    105 head. Things on the left and right of `->` are called LHS and RHS of an
    106 injectivity condition, respectively. The user must be able to name the result of
    107 a type family. To achieve that we extend syntax of type family head by allowing
    108 to write `= tyvar` or `= (tyvar :: kind)` annotations in addition to already
     83When deciding on a concrete syntax our two main design goals were:
     84
     85  * '''Backwards compatibility''': injective type families are automatically
     86    enabled with the `TypeFamilies` language extension. This means that the
     87    proposed syntax had to be backward compatible, ie. not break any existing
     88    code that uses type families.
     89
     90  * '''Future extensibility''': currently we we only implemented injectivity A
     91    and B but we still want to be able to implement injectivity C in the future
     92    without breaking A and B.
     93
     94We decided to use syntax borrowed from functional dependencies.  First of all
     95the user must be able to introduce a variable that names the result of a type
     96family.  To achieve that we extend syntax of type family head by allowing to
     97write `= tyvar` or `= (tyvar :: kind)` annotations in addition to already
    10998allowed `:: kind` annotation. In other words all these declaration are
    11099well-formed:
     
    118107
    119108but the third or fourth form is required if the user wants to introduce
    120 injectivity declaration. Here are examples of injectivity declarations using
    121 proposed syntax:
    122 
    123 {{{#!hs
    124 type family Id a = result | result -> a where
    125 type family F a b c = d | d -> a b c
    126 type family G a b c = foo | foo -> a b where
     109injectivity annotation. The injectivity annotation itself begins with `|`
     110following the result type variable.  `|` is followed by an injectivity
     111condition. Injectivity condition has the form:
     112
     113{{{#!hs
     114A -> B
     115}}}
     116
     117where `A` is the result type variable and `B` is a non-empty lists of type
     118variables declared in type family head. Things on the left and right of `->` are
     119called LHS and RHS of an injectivity condition, respectively. If a type family
     120is injective in a given argument respective type variable must be mentioned in
     121the RHS of an injectivity condition. Variables may be skipped if a type family
     122is not injective in a given argument.
     123
     124Here are examples of injectivity declarations using proposed syntax:
     125
     126{{{#!hs
     127type family Id a = result | result -> a where { ... }
     128type family F a b c = d | d -> c a b
     129type family G a b c = foo | foo -> a b where { ... }
     130}}}
     131
     132This syntax can be easily extended in the future if we want to implement
     133injectivity of type C. First required change is that there may be many
     134comma-separated injectivity conditions.  Second change is that LHS of
     135injectivity condition can mention type variables that name the arguments, not
     136just the result.  With this extended syntax we could write:
     137
     138{{{#!hs
    127139type family Plus a b = (sum :: Nat) | sum a -> b, sum b -> a where
    128140type family H a b c = xyz | xyz a -> b c, xyz b -> a c
    129141}}}
    130142
    131 Note that above examples demonstrate all three types of injectivivity but for
    132 now we only plan to implement injectivity A.
    133 
    134 Pros:
    135 
    136   * natural reading: `res a -> b` reads as "knowing res and a determines b".
    137 
    138   * extensible for the future
    139 
    140   * backwards compatible
    141 
    142 Cons:
    143 
    144   * since we only plan to implement injectivity of form A we require that there
    145     is only one injectivity condition, its LHS contains only a type variable
    146     naming the result and its RHS contains all type variables naming the
    147     arguments to a type family. This might be a bit annoying.
    148 
    149 
    150 == Real-life use cases
    151 
    152 ''If you can supply more examples (type family declarations + their usage that
    153 currently doesn't work but should work with injectivity) please add them here.''
    154 
    155 '''Example 1'''
    156 
    157 {{{#!hs
    158 type family F a = result | result -> a where
    159     F Char = Bool
    160     F Bool = Char
    161     F a    = a
    162 
    163 idChar :: (F a ~ Bool) => a -> Char
    164 idChar a = a
    165 
    166 idDouble :: (F b ~ Double) => b -> Double
    167 idDouble a = a
    168 }}}
    169 
    170 GHC should infer that `a` is in fact `Char` and `b` is `Double`. Right now this program is rejected.
    171 
    172 '''Example 2''' (taken from [ticket:6018#comment:5])
    173 
    174 {{{#!hs
    175 data Nat
    176     = Zero
    177     | Suc Nat
    178 
    179 data CoNat
    180     = Co Nat
    181     | Infinity
    182 
    183 type family Succ (t ::  CoNat) :: CoNat
    184 type instance Succ (Co n)           = Co (Suc n)
    185 type instance Succ Infinity         = Infinity
    186 }}}
    187 
    188 GHC can't infer `Succ n ~ Succ m => n ~ m` because it can't see that `Succ` is injective.
    189 
    190 '''Example 3''' (taken from [ticket:6018#comment:26])
    191 
    192 {{{#!hs
    193 class Manifold' a where
    194     type Field a
    195     type Base  a
    196     type Tangent a
    197     type TangentBundle a
    198     type Dimension a ::  Nat
    199     type UsesMetric a :: Symbol
    200     project :: a -> Base a
    201     unproject :: Base a -> a
    202     tangent :: a -> TangentBundle a
    203     cotangent :: a -> (TangentBundle a -> Field a)
    204 
    205 -- this works
    206 id' :: forall a. ( Manifold' a ) => Base a -> Base a
    207 id' input = project out
    208   where
    209     out :: a
    210     out = unproject input
    211 
    212 -- but this requires injective type families
    213 id' :: forall a. ( Manifold' a ) => Base a -> Base a
    214 id' = project . unproject
    215 
    216 }}}
     143Note that for open and closed type families it is correct to declare a type
     144variable that names the result but skip the injectivity annotation.  That is
     145not the case for associated types.  If you name the result but ignore the
     146injectivity annotation GHC will interpret this as an associated type default.
    217147
    218148== Implementation outline
    219149
    220 === Verifying correctness of user's injectivity declaration
     150=== Verifying correctness of injectivity annotation
     151
     152Before checking that a type family is indeed injective, as declared by the user,
     153GHC needs to check the correctness of injectivity annotation itself.  This
     154includes checking that:
     155
     156  * only in-scope type variables are used. For example
     157    `type family F a = r | r -> b` should result with "not in scope: b" error.
     158
     159See test T6018rnfail in the testsuite for more examples of invalid declarations.
     160
     161=== Verifying that type family equations agree with injectivity annotation
    221162
    222163Once the user declares type family to be injective GHC must verify that this
    223 declaration is correct, ie. type family really is injective. Below is an outline
    224 of the algorithm. It is then follow with a discussion and rationale. ''Note: I
    225 am not too familiar with GHC's type checking so please tell me if I'm making any
    226 wrong assumptions here. Also, I might be using incorrect terminology. If so
    227 please complain or fix.''
    228 
    229 '''Important''': this algorithm is only for the injectivity of type A. RHS
    230 refers to the right-hand side of the type family being checked for
    231 injectivity. LHS refers to the arguments of that type family.
    232 
    233 '''Algorithm'''
    234 
    235 1. If a RHS contains a call to a type family we conclude that the type family is
    236    not injective. I am not certain if this extends to self-recursion -- see
    237    discussion below.
    238 
    239 Open type families:
    240 
    241 2. When checking equation of an open type family we try to unify its RHS with
    242    RHSs of all equations we've seen so far. If we succeed then LHSs of unified
    243    equations must be identical under that substitution. If they are not identical
    244    then we declare that a type family is not injective.
    245 
    246 '''RAE:''' I believe this would also have to check that all variables mentioned in the LHS are mentioned in the RHS. Or, following along with Simon's idea in comment:76:ticket:6018, those variables that appear in the injectivity annotation must be mentioned in the RHS. '''End RAE'''
    247 
    248 Closed type families
    249 
    250 3. If a type family has only one equation we declare it to be injective (unless
    251    case 1 above applies). '''RAE''' or there are variables missing from the RHS '''End RAE'''
    252 
    253 4. If a type family has more equations then we check them one by one. Checking
    254    each equation consists of these steps:
    255 
    256   0) verify 1) for the current equation.
    257 
    258   a) attempt to unify RHS with RHSs of all previous equations. If this does not
    259   succeed proceed to next equation. If this was the last equation then type
    260   family is injective.
    261 
    262   b) if unification in a) succeeds and no substitutions are required then type
    263   family is not injective and we report an error to the user. By "no
    264   substitution" I mean situation when there are no type variables involved
    265   ie. both sides declare the same concrete type (eg. Int). '''RAE''' This seems to be a straightforward special case of (c). Omit? '''End RAE'''
    266 
    267   c) if unification succeeds and there are type variables involved we substitute
    268   unified type variables on the LHS and check whether this LHS overlaps with
    269   any of the previous equations. If it does we proceed to the next equation
    270   (if this was the last equation then type family is injective). If it
    271   doesn't then type family is not injective and we report an error to the
    272   user. See examples and discussion below for more details.
    273 
    274 '''RAE:''' We have to be careful with the word ''overlap'' here. I think we want "overlaps" to be "is subsumed by".
    275 
    276 Even subtler, it's possible that certain values for type variables are excluded if the current LHS is reachable (for example, some variable `a` couldn't be `Int`, because if `a` were `Int`, then a previous equation would have triggered). Perhaps these exclusions can also be taken into account. Thankfully, forgetting about the exclusions is conservative -- the exclusions can only make ''more'' families injective, not ''fewer''. '''End RAE'''
    277 
    278 '''RAE's examples'''
    279 
    280 {{{#!hs
    281 type family E2 (a :: Bool) = r | r -> a where
    282   E2 False = True
    283   E2 True  = False
    284   E2 a     = False
    285 }}}
    286 
    287 A naive injectivity check here would conclude that `E2` is not injective, because the RHS of the last equation unifies with the RHS of a previous equation, and the LHS of the last equation is not subsumed by any previous equation. But, noting that `a` (as used in the last equation) can neither be `True` nor `False`, `E2 is in fact injective. These are the "exclusions" I talk about above.
    288 
    289 '''Discussion'''
    290 
    291 Case 1 above is conservative and may incorrectly reject injectivity declaration
    292 for some type families. For example type family `I`:
    293 
    294 {{{#!hs
    295 type family I a = r | r -> a where
    296      I a = Id a -- Id defined earlier
    297 }}}
    298 
    299 is injective but restriction in case 1 will reject it. Why such a restriction?
    300 Consider this example. Let us assume that we have type families `X` and `Y` that
    301 we already know are injective, and type constructors `Bar :: * -> *` and
    302 `Baz :: * -> * -> *`. Now we declare:
    303 
    304 {{{#!hs
    305 type family Foo a = r | r -> a where
    306      Foo (Bar a)   = X a
    307      Foo (Baz a b) = Y a b
    308 }}}
    309 
    310 Here we would need to check whether results of `X a` and `Y a b` can overlap and
    311 I don't see a good way of doing this once the RHS has nested calls to type
    312 families. Second of all if we see `Foo a ~ Bool` during type checking GHC can't
    313 solve that without trying each equation one by one to see which one returns
    314 `Bool`. This takes a lot of guessing and I believe GHC should refuse to do that.
    315 See also #4259.
    316 
    317 What about self-recursion? Consider this type family:
    318 
    319 {{{#!hs
    320 -- assumes promoted Maybe and Nat
    321 type family NatToMaybe a = r | r -> a where
    322      NatToMaybe Z     = Nothing
    323      NatToMaybe (S n) = Just (NatToMaybe n)
    324 }}}
    325 
    326 Using Case 4a we will infer correctly that this type family is injective. Now
    327 consider this:
    328 
    329 {{{#!hs
    330 type family Ban a = r | r -> a where
    331      Ban Z     = Z
    332      Ban (S n) = Ban n
    333 }}}
    334 
    335 To verify injectivity in this case we need to ask whether `Z ~ Ban n` (case 4a
    336 above). We can only answer such question when a type family is injective. Here
    337 we have not confirmed that `Ban` is injective so we may rightly refuse to answer
    338 `Z ~ Ban n` and conclude (correctly) that this type family is not injective. So it
    339 seems to me that we could allow self-recursion - I have not yet identified any
    340 corner cases that would prevent us from doing so.
    341 
    342 '''RAE:''' But it seems that, under this treatment, any self-recursion would automatically lead to a conclusion of "not injective", just like any other use of a type family. For example:
    343 
    344 {{{#!hs
    345 type family IdNat n = r | r -> a where
    346   IdNat Z = Z
    347   IdNat (S n) = S (IdNat n)
    348 }}}
    349 
    350 `IdNat` is injective. But, following the algorithm above, GHC would see the recursive use of `IdNat`, not know whether `IdNat` is injective, and then give up, concluding "not injective". Is there a case where the special treatment of self-recursion leads to a conclusion of "injective"? '''End RAE'''
    351 
    352 Here's an example of case 4c in action:
    353 
    354 {{{#!hs
    355 type family Bak a = r | r -> a where
    356      Bak Int  = Char
    357      Bak Char = Int
    358      Bak a    = a
    359 }}}
    360 
    361 Equation 2 falls under case 4a. When we reach equation 3 we attempt to verify
    362 it's RHS with each RHS of the previous equations. Attempt to unify `a` with
    363 `Char` succeeds. Since unification was successful we substitute `Char` on the LHS
    364 of the 3rd equation and get `Bak Char`. Now we must check if this equation
    365 overlaps with any of the previous equations. It does overlap with the second
    366 one, so everything is fine: we know that 3rd equation will never return a `Char`
    367 (like 1st equation) because this case will be caught by the 2nd equation. We
    368 know repeat the same steps for the second equations and conclude that 3rd
    369 equation will never produce an `Int` because this will be caught by the 1st
    370 equation. We thus conclude that `Bak` is injective.
    371 
    372 === Other implementation details
    373 
    374 The implementation needs to check the correctness of injectivity conditions
    375 declarations. This includes checking that:
    376 
    377   * only in-scope type variables are used. For example
    378     `type family F a | result -> b` should result with "not in scope: b" error.
     164declaration is correct, ie. type family really is injective.  Below are the
     165rules we follow when checking for injectivity of a type family. For full details
     166and rationale behind them see the injectivity paper, Section 4.2.
     167
     168'''Important''': these rules are only for the currently implemented injectivity
     169of types A and B.  RHS refers to the right-hand side of the type family equation
     170being checked for injectivity.  LHS refers to the arguments of that type family
     171equation.  Term "type family equation" can refer to equations of both open and
     172closed type families, unless stated otherwise.
     173
     174'''Rules for checking injectivity'''
     175
     176A general idea is that if we find at least one equation (bullets (1), (2) and
     177(3)) or a pair of equations (bullets (4) and (5)) that violate injectivity
     178annotation then we conclude that a type family is not injective in a way user
     179claims and we report an error.
     180
     1811. If a RHS of a type family equation is a type family application we conclude
     182   that the type family is not injective.
     183
     1842. If a RHS of a type family equation is a bare type variable we require that
     185   all LHS variables (including implicit kind variables) are also bare.  In
     186   other words, this has to be a sole equation of that type family and it has to
     187   cover all possible patterns.  If the patterns are not covering we conclude
     188   that the type family is not injective.
     189
     1903. If a LHS type variable that is declared as injective is not mentioned on
     191   injective position in the RHS we conclude that the type family is not
     192   injective.  By "injective position" we mean argument to a type constructor or
     193   argument to a type family on injective position.
     194
     195__Open type families (including associated types)__
     196
     197Open type families are typechecked incrementally.  This means that when a module
     198is imported type family instances contained in that module are checked against
     199instances present in already imported modules.  In practice this is done by
     200checking equations pair-wise (a new equation against all already checked
     201equations -- modulo optimisations).
     202
     2034. When checking a pair of an open type family equations we attempt to unify
     204   their RHSs. If they don't unify this pair does not violate injectivity
     205   annotation.  If unification succeeds with a substitution (possibly empty)
     206   then LHSs of unified equations must be identical under that substitution. If
     207   they are not identical then we conclude that a type family is not injective.
     208
     209Note that we use a special variant of the unification algorithm that treats type
     210family applications as possibly unifying with anything.
     211
     212__Closed type families__
     213
     214In a closed type family all equations are ordered and in one place. Equations
     215are also checked pair-wise but this time an equation has to be paired with all
     216the preceeding equations.  Of course a single-equation closed type family is
     217trivially injective (unless (1), (2) or (3) above holds).
     218
     2195. When checking a pair of closed type family equations we try to unify their
     220   RHSs.  If they don't unify this pair does not violate injectivity annotation.
     221   If the RHSs can be unified under some substitution (possibly empty) then
     222   either the LHSs unify under the same substitution or the LHS of the latter
     223   equation is subsumed by earlier equations.  If neither condition is met we
     224   conclude that a type family is not injective.
     225
     226Again, we use a special variant of the unification algorithm.
     227
     228=== Source code tour
     229
     230Below is a list of primary source code locations that implement injectivity:
     231
     232  * [[GhcFile(compiler/rename/RnSource.hs)]].`rnInjectivityAnn`: checks
     233    correctness of injectivity annotation (mostly variable scoping).
     234
     235  * [[GhcFile(compiler/typecheck/FamInst.hs)]].`checkForInjectivityConflicts` is
     236    an entry point for injectivity check of open type families.
     237
     238  * [[GhcFile(compiler/typecheck/TcTyClsDecls.hs)]].`checkValidClosedCoAxiom` is
     239    an entry point for injectivity check of closed type families.
     240
     241  * [[GhcFile(compiler/types/FamInstEnv.hs)]].`injectiveBranches` checks that a
     242    pair of type family axioms does not violate injectivity annotation.
     243
     244  * [[GhcFile(compiler/types/FamInstEnv.hs)]].`lookupFamInstEnvInjectivityConflicts`
     245    implements condition (4) of injectivity check.
     246
     247  * [[GhcFile(compiler/typecheck/TcTyClsDecls.hs)]].`checkValidClosedCoAxiom.check_injectivity.gather_conflicts`
     248    implements condition (5) of injectivity check.
     249
     250  * [[GhcFile(compiler/types/Unify.hs)]].`tcUnifyTyWithTFs` is our special
     251    variant of a unification algorithm.
     252
     253  * [[GhcFile(compiler/typecheck/FamInst.hs)]].`makeInjectivityErrors` checks
     254    conditions (1), (2) and (3) of the injectivity check.  It also takes as an
     255    argument results of check (4) or (5) and constructs error messages, if
     256    necessary.
     257
     258  * [[GhcFile(compiler/typecheck/TcInteract)]], functions
     259    `improveLocalFunEqs.do_one_injective` and `improve_top_fun_eqs` implement
     260    typechecking improvements based on injectivity information.
     261
     262Relevant source code notes are:
     263
     264  * `Note [FamilyResultSig]` in [[GhcFile(compiler/hsSyn/HsDecls.hs)]]
     265  * `Note [Injectivity annotation]` in [[GhcFile(compiler/hsSyn/HsDecls.hs)]]
     266  * `Note [Injective type families]` in [[GhcFile(compiler/types/TyCon.hs)]]
     267  * `Note [Renaming injectivity annotation]` in [[GhcFile(compiler/rename/RnSource.hs)]]
     268  * `Note [Verifying injectivity annotation]` in [[GhcFile(compiler/types/FamInstEnv.hs)]]
     269  * `Note [Type inference for type families with injectivity]` in [[GhcFile(compiler/typecheck/TcInteract.hs)]]
     270
     271
     272== Injectivity for poly-kinded type families
     273
     274With ''PolyKinds'' extension enabled it is possible to declare kind variables as
     275injective.  Moreover, if a type variable is declared as injective its associated
     276kind variable is also considered injective.  See section 6 of the injectivity
     277paper for full details.
     278
     279== Connection with functional dependencies
     280
     281In the course of our work it turned out that there is a close correspondence
     282between injective type families and functional dependencies.  Section 7 of
     283the injectivity paper discusses this connection.
     284
     285== Future plans and ideas
     286
     287=== Type C injectivity
     288
     289Our plan for the nearest future is to implement injectivity of type C.  This
     290will give injective type families expressive power identical to this of
     291functional dependencies.
     292
     293If we decied to implement injectivity of type C checking injectivity annotation
     294would become more complicated as we would have to check for things like:
     295
     296  * `type family F a b = r | r -> a, r -> b`. This is technically correct but we
     297    could just say `result -> a b`.
    379298
    380299  * there are no identical conditions (this wouldn't hurt, but the user deserves
     
    382301
    383302  * type variables are not repeated on either LHS or RHS of the injectivity
    384     condition. For example `result a a -> ...` or `... -> a b a` should generate
     303    condition. For example `r a a -> ...` or `... -> a b a` should generate
    385304    a warning. Note that it probably is OK to have the same variable both on the
    386305    LHS and RHS of an injectivity condition: in the above examples it is true
     
    391310    `result -> a`). This probably deserves a warning.
    392311
    393 I am not certain at the moment how to treat these injectivity conditions
    394 declarations:
    395 
    396   * `result -> a, result -> b` is technically correct but we could just say
    397     `result -> a b`. Do the two separate declarations have the same power as the
    398     combined one?
    399 
    400312=== Inferring injectivity
    401313
    402314[ticket:6018#comment:45 Here] it was suggested by Simon that we could infer
    403 injectivity for closed type families. This is certainly possible for injectivity
    404 A, but not for B or C, where the number of possible injectivity conditions is
    405 exponential in the number of arguments. I personally am against inferring
    406 injectivity. The reasons are:
    407 
    408   * Before 7.10 comes out there will already be some code in the wild that uses
     315injectivity for closed type families. I initially argued that, while inferring
     316injectivity of type A should be simple, inferring injectivity of type B would be
     317exponential in the numer of arguments to a type family. I take back that claim
     318as I now believe the algorithm can be made linear in the number of
     319arguments. Say we have a closed type family:
     320
     321{{{#!hs
     322type family F a b c ... n = r where
     323}}}
     324
     325Since there are n arguments there are 2^n possible injectivity annotations.
     326That's why I believed that we have to check every possible annotationton.  I now
     327believe that instead checking every possible annotation we should only check
     328whether knowing the RHS allows to infer each argument independently.  In other
     329words when inferring injectivity we would check whether annotations `r -> a`, `r
     330-> b`, `r -> c` ... `r -> n` hold true. If we learn for example that knowing `r`
     331allows to infer `a`, `c` and `n` but not the other argumenst we infer the
     332annotation `r -> a c n`.
     333
     334There are several concerns to consider before implementing this:
     335
     336  * Before GHC 8.0 comes out there will already be some code in the wild that uses
    409337    closed type families introduced in GHC 7.8. None of these type families
    410338    require injectivity to work because GHC 7.8 does not support injectivity. If
     
    416344
    417345  * I believe that requiring explicit injectivity annotations is a valuable
    418     source code documentation for the programmer.
    419 
    420   * Annotations also make it explicit which code will compile with GHC 7.10 and
    421     which will not.
     346    source code documentation for the programmer.  This is very subjective, but
     347    the truth is injectivity is very subtle and can easily be broken by slight
     348    modifications of type family definition.  It is much better to be explicit
     349    about relying on injectivity.
     350
     351  * Annotations also make it explicit which code compiles with GHC 8.0 and
     352    which does not. If we infer injectivity the code that works with 8.0 might
     353    result in typing errors for earlier GHC versions. Of course requiring
     354    annotations will also prevent that code from compiling but I believe that it
     355    will be easier for the programmer to track the source of the problem when
     356    she gets syntax errors rather than typing errors.
    422357
    423358  * I don't like the idea of mismatch between open type families and closed type
    424359    families, meaning that injectivity of open type families would be openly
    425360    documented whereas for closed type families it would be hidden.
    426 
    427 == Injectivity for poly-kinded type families
    428 
    429 (based on Richard's comments on Phab)
    430 
    431 Current implementation of injectivity only works over *type* variables, ignoring *kind* variables. This is OK because all kind variables have to have type variables dependent on them, and if a type family is injective in its type variables, it then must be injective in its kind variables. But, if/when we allow partial injectivity annotations, this might require some more thought. Consider
    432 
    433 {{{
    434 type family Foo (a :: k) (b :: *) = (r :: k) | r -> b
    435 }}}
    436 
    437 That family is injective in `k`, but you have to be careful to discover this fact. And, what about
    438 
    439 {{{
    440 type family Bar (a :: k) = r | r -> a
    441 }}}
    442 
    443 Here, the family is still injective in `k`, but you need to make sure to note it when recording the partial injectivity.
    444 
    445 Currently we disallow:
    446 
    447 {{{
    448 type family Baz (a :: k) = r | r -> k
    449 }}}
    450 
    451 But such a thing is reasonable to want! You're saying that result determines the kind of the input, though perhaps not the type.
    452 
    453 
    454 == Other notes
    455 
    456   * This page does not mention anything about associated types. The intention is
    457     that injectivity will also work for those. I just haven't thought about the
    458     details yet.
    459 
    460   * [ticket:6018#comment:48 Here] Richard mentions head-injectivity used by
    461     Agda. We don't plan to follow that direction.
    462 
    463   * I'm not yet sure what is the exact scope of things we want to do with
    464     injectivity. Certainly if we have `F a ~ F b` and `F` is injective then we
    465     can declare `a ~ b`. (Note: Simon remarks that in such case `a` must be a
    466     skolem constant and `b` a unification variable. I don't know the difference
    467     between the two). Moreover if we have `F a ~ Int` then we can infer `a`. But
    468     what if we also have injective type family `G` and see a constraint like
    469     `F a ~ G b c`? For injective type families there exists at most one solution
    470     but I think that GHC should refuse to solve such riddles.
     361    Counterargument: there is already a mismatch between open and closed type
     362    families, since the latter have kind inference.
     363
     364  * If we ever implement injectivity of type C it might not be possible to infer
     365    injectivity annotation of type C.  I think that this time the algorithm will
     366    really be exponential.
     367
     368== Example use cases
     369
     370In the injectivity paper we presented two practical use cases for injectivity.
     371If you have more uses cases to demonstrate please add them here.
     372