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

 If we're not aiming to get this into 7.10 then I guess there's no rush.

 Replying to [comment:93 simonpj]:
 > All I plan to do is add a rule along the lines of
 > {{{
 >   [W] F ty1 ~ rhs
 >   [W] F ty2 ~ rhs
 > ===>  add a new constraint (if F is injective)
 >   [D] ty1 ~ ty2
 > }}}
 > very like functional dependencies for type classes.
 Yes, that's what I meant with my INJFEQFEQ interaction rule in [comment:89
 comment 89]:
 {{{
 INJFEQFEQ   interact[l] (F \vec{Xi_1} ~ Xi, F \vec{Xi_2} ~ Xi) =
                         (F \vec{Xi_1} ~ Xi, \vec{ Xi_1 ~ Xi_2 })
 }}}
 Sorry if that wasn't clear. (Now I realized that checking whether `F` is
 injective might be consider a reaction with top-level axiom and thus this
 should be a reaction rule.)

 But it seems to me there should be one more rule. Consider this example:

 {{{#!hs
 type family F a = r | r -> a where
     F Char = Bool
     F Bool = Char
     F a    = a

 idChar :: (F a ~ Bool) => a -> Char
 idChar a = a
 }}}

 Here we have constraint `F a ~ Bool`. Knowing that `F` is injective and
 it's RHS is `Bool` we want to deduce that `a` must be `Char`. This one
 seems more difficult because we have to look through all the equations. My
 guess would be that when we have to do this before constraint solving (in
 `TcM` monad?).

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