[GHC] #7377: Type equality unification shortcoming

[GHC]

#7377: Type equality unification shortcoming
---------------------------------------+------------------------------------
 Reporter:  acowley                    |          Owner:                  
     Type:  bug                        |         Status:  new             
 Priority:  normal                     |      Component:  Compiler        
  Version:  7.6.1                      |       Keywords:                  
       Os:  Unknown/Multiple           |   Architecture:  Unknown/Multiple
  Failure:  GHC rejects valid program  |       Testcase:                  
Blockedby:                             |       Blocking:                  
  Related:                             |  
---------------------------------------+------------------------------------
 The following program demonstrates cases where the equality `f a ~ g b` is
 not enough for the type checker to deduce `f ~ g` and `a ~ b`.

 {{{
 {-# LANGUAGE GADTs, TypeOperators, KindSignatures, PolyKinds,
 TypeFamilies, RankNTypes #-}
 data a :=: b where Refl :: a :=: a
 type family Arg x
 type instance Arg (f x) = x
 type family Func (x :: *) :: * -> *
 type instance Func (f x) = f

 congArg :: x :=: y -> Arg x :=: Arg y
 congArg Refl = Refl
 congFunc :: x :=: y -> Func x :=: Func y
 congFunc Refl = Refl
 inversion :: forall (f :: * -> *)(g :: * -> *)(a :: *)(b :: *).
              f a :=: g b -> (f :=: g , a :=: b)
 --inversion Refl = (Refl, Refl) -- Doesn't type check!
 inversion eq = (congFunc eq , congArg eq) -- Does type check

 -- Even simpler example that doesn't type check
 -- foo :: f a ~ g b => f () -> g ()
 -- foo x = x
 }}}

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7377>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler