Changes between Version 23 and Version 24 of InjectiveTypeFamilies

Sep 3, 2015 4:45:13 AM (4 years ago)

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


  • InjectiveTypeFamilies

    v23 v24  
    11= Injective type families
    3 This page summarizes the design behind injective type families (#6018). For the latest information about implementation progress see [[|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.
    5 Person responsible for this page and the implementation: Jan Stolarek (just so
    6 you now who is meant by "I").
    8 My current implementation is located on GitHub:
    10   *
    11   *
    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[[|Phab D202]].
     7As of September 2015 injective type families are merged into HEAD and will be
     8available in the next stable GHC release (8.0).
     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").
    1518== Forms of injectivity
    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:
    2023  A. Injectivity in all the arguments, where knowing the result (right-hand
    5457type family Plus a b where
    55      Plus Z      n = n
    56      Plus (S m ) n = S (Plus n m)
    57 }}}
    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)
     62  Here knowing the RHS and the first argument uniquely determines the remaining
     63  argument.
    7073  about `a` or `b`.
    7375In the following text I will refer to these three forms of injectivity as A, B
    7476and C.
    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).
    8081== Proposed syntax
    82 Two important things to consider when deciding on a concrete syntax are:
    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).
    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.
    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:
    100 {{{#!hs
    101 A -> B
    102 }}}
    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:
     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.
     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.
     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
    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:
    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:
     114A -> B
     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.
     124Here are examples of injectivity declarations using proposed syntax:
     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 { ... }
     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:
    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
    131 Note that above examples demonstrate all three types of injectivivity but for
    132 now we only plan to implement injectivity A.
    134 Pros:
    136   * natural reading: `res a -> b` reads as "knowing res and a determines b".
    138   * extensible for the future
    140   * backwards compatible
    142 Cons:
    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.
    150 == Real-life use cases
    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.''
    155 '''Example 1'''
    157 {{{#!hs
    158 type family F a = result | result -> a where
    159     F Char = Bool
    160     F Bool = Char
    161     F a    = a
    163 idChar :: (F a ~ Bool) => a -> Char
    164 idChar a = a
    166 idDouble :: (F b ~ Double) => b -> Double
    167 idDouble a = a
    168 }}}
    170 GHC should infer that `a` is in fact `Char` and `b` is `Double`. Right now this program is rejected.
    172 '''Example 2''' (taken from [ticket:6018#comment:5])
    174 {{{#!hs
    175 data Nat
    176     = Zero
    177     | Suc Nat
    179 data CoNat
    180     = Co Nat
    181     | Infinity
    183 type family Succ (t ::  CoNat) :: CoNat
    184 type instance Succ (Co n)           = Co (Suc n)
    185 type instance Succ Infinity         = Infinity
    186 }}}
    188 GHC can't infer `Succ n ~ Succ m => n ~ m` because it can't see that `Succ` is injective.
    190 '''Example 3''' (taken from [ticket:6018#comment:26])
    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)
    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
    212 -- but this requires injective type families
    213 id' :: forall a. ( Manifold' a ) => Base a -> Base a
    214 id' = project . unproject
    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.
    218148== Implementation outline
    220 === Verifying correctness of user's injectivity declaration
     150=== Verifying correctness of injectivity annotation
     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:
     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.
     159See test T6018rnfail in the testsuite for more examples of invalid declarations.
     161=== Verifying that type family equations agree with injectivity annotation
    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.''
    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.
    233 '''Algorithm'''
    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.
    239 Open type families:
    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.
    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'''
    248 Closed type families
    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'''
    253 4. If a type family has more equations then we check them one by one. Checking
    254    each equation consists of these steps:
    256   0) verify 1) for the current equation.
    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.
    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'''
    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.
    274 '''RAE:''' We have to be careful with the word ''overlap'' here. I think we want "overlaps" to be "is subsumed by".
    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'''
    278 '''RAE's examples'''
    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 }}}
    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.
    289 '''Discussion'''
    291 Case 1 above is conservative and may incorrectly reject injectivity declaration
    292 for some type families. For example type family `I`:
    294 {{{#!hs
    295 type family I a = r | r -> a where
    296      I a = Id a -- Id defined earlier
    297 }}}
    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:
    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 }}}
    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.
    317 What about self-recursion? Consider this type family:
    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 }}}
    326 Using Case 4a we will infer correctly that this type family is injective. Now
    327 consider this:
    329 {{{#!hs
    330 type family Ban a = r | r -> a where
    331      Ban Z     = Z
    332      Ban (S n) = Ban n
    333 }}}
    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.
    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:
    344 {{{#!hs
    345 type family IdNat n = r | r -> a where
    346   IdNat Z = Z
    347   IdNat (S n) = S (IdNat n)
    348 }}}
    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'''
    352 Here's an example of case 4c in action:
    354 {{{#!hs
    355 type family Bak a = r | r -> a where
    356      Bak Int  = Char
    357      Bak Char = Int
    358      Bak a    = a
    359 }}}
    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.
    372 === Other implementation details
    374 The implementation needs to check the correctness of injectivity conditions
    375 declarations. This includes checking that:
    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.
     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.
     174'''Rules for checking injectivity'''
     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.
     1811. If a RHS of a type family equation is a type family application we conclude
     182   that the type family is not injective.
     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.
     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.
     195__Open type families (including associated types)__
     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).
     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.
     209Note that we use a special variant of the unification algorithm that treats type
     210family applications as possibly unifying with anything.
     212__Closed type families__
     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).
     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.
     226Again, we use a special variant of the unification algorithm.
     228=== Source code tour
     230Below is a list of primary source code locations that implement injectivity:
     232  * [[GhcFile(compiler/rename/RnSource.hs)]].`rnInjectivityAnn`: checks
     233    correctness of injectivity annotation (mostly variable scoping).
     235  * [[GhcFile(compiler/typecheck/FamInst.hs)]].`checkForInjectivityConflicts` is
     236    an entry point for injectivity check of open type families.
     238  * [[GhcFile(compiler/typecheck/TcTyClsDecls.hs)]].`checkValidClosedCoAxiom` is
     239    an entry point for injectivity check of closed type families.
     241  * [[GhcFile(compiler/types/FamInstEnv.hs)]].`injectiveBranches` checks that a
     242    pair of type family axioms does not violate injectivity annotation.
     244  * [[GhcFile(compiler/types/FamInstEnv.hs)]].`lookupFamInstEnvInjectivityConflicts`
     245    implements condition (4) of injectivity check.
     247  * [[GhcFile(compiler/typecheck/TcTyClsDecls.hs)]].`checkValidClosedCoAxiom.check_injectivity.gather_conflicts`
     248    implements condition (5) of injectivity check.
     250  * [[GhcFile(compiler/types/Unify.hs)]].`tcUnifyTyWithTFs` is our special
     251    variant of a unification algorithm.
     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.
     258  * [[GhcFile(compiler/typecheck/TcInteract)]], functions
     259    `improveLocalFunEqs.do_one_injective` and `improve_top_fun_eqs` implement
     260    typechecking improvements based on injectivity information.
     262Relevant source code notes are:
     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)]]
     272== Injectivity for poly-kinded type families
     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.
     279== Connection with functional dependencies
     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.
     285== Future plans and ideas
     287=== Type C injectivity
     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.
     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:
     296  * `type family F a b = r | r -> a, r -> b`. This is technically correct but we
     297    could just say `result -> a b`.
    380299  * there are no identical conditions (this wouldn't hurt, but the user deserves
    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.
    393 I am not certain at the moment how to treat these injectivity conditions
    394 declarations:
    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?
    400312=== Inferring injectivity
    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:
    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:
     322type family F a b c ... n = r where
     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`.
     334There are several concerns to consider before implementing this:
     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
    417345  * I believe that requiring explicit injectivity annotations is a valuable
    418     source code documentation for the programmer.
    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.
     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.
    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.
    427 == Injectivity for poly-kinded type families
    429 (based on Richard's comments on Phab)
    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
    433 {{{
    434 type family Foo (a :: k) (b :: *) = (r :: k) | r -> b
    435 }}}
    437 That family is injective in `k`, but you have to be careful to discover this fact. And, what about
    439 {{{
    440 type family Bar (a :: k) = r | r -> a
    441 }}}
    443 Here, the family is still injective in `k`, but you need to make sure to note it when recording the partial injectivity.
    445 Currently we disallow:
    447 {{{
    448 type family Baz (a :: k) = r | r -> k
    449 }}}
    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.
    454 == Other notes
    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.
    460   * [ticket:6018#comment:48 Here] Richard mentions head-injectivity used by
    461     Agda. We don't plan to follow that direction.
    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.
     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.
     368== Example use cases
     370In the injectivity paper we presented two practical use cases for injectivity.
     371If you have more uses cases to demonstrate please add them here.