id,summary,reporter,owner,description,type,status,priority,milestone,component,version,resolution,keywords,cc,os,architecture,failure,difficulty,testcase,blockedby,blocking,related
7377,Type equality unification shortcoming,acowley,,"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
}}}",bug,closed,normal,,Compiler,7.6.1,fixed,,sanzhiyan@… djahandarie@…,Unknown/Multiple,Unknown/Multiple,GHC rejects valid program,Unknown,,,,