#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
_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
