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