# Changes between Version 16 and Version 17 of InjectiveTypeFamilies

Ignore:
Timestamp:
Oct 14, 2014 1:59:09 AM (5 years ago)
Comment:

--

Unmodified
Added
Removed
Modified
• ## InjectiveTypeFamilies

 v16 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''' '''RAE's examples''' Here are some examples that I've come up with that show some tricky points: {{{#!hs type family E1 a = r | r -> a where E1 Int = Int E1 a   = a }}} According to the algorithm above, this would be rejected as non-injective. This is because clause (c) of the closed type family check says that if an equation is not subsumed by a previous equation, yet the RHSs unify, the family is flagged as non-injective. Yet, `E1` ''is'' injective. Here's another one: {{{#!hs type family E2 (a :: Bool) = r | r -> a where E2 False = True E2 True  = False E2 a     = False }}} 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. '''Discussion'''