id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc	os	architecture	failure	difficulty	testcase	blockedby	blocking	related
7205	Re-introduce left/right coercion decomposition	simonpj		"Suppose we have
{{{
data T a where
  MkT :: f a -> T (f a)
  ...other constructors...

foo :: T (f a) -> f a
foo (MkT x) = x
}}}
You might think this would obviously be OK, but currently we get
{{{
Foo.hs:10:15:
    Could not deduce (a1 ~ a)
    from the context (f a ~ f1 a1)
      bound by a pattern with constructor
                 MkT :: forall (f :: * -> *) a. f a -> T (f a),
               in an equation for `foo'
      at Foo.hs:10:6-10
}}}
Reason: we don't have the left/right decomposition rules for coercions, which were in an earlier version.  (In fact this does compile with GHC 7.0.)  We removed them (a) because we were interested in supporting un-saturated type functions, and (b) we didn't think it was that important.

But in fact it IS an annoying problem.  A recent example is [http://www.mail-archive.com/haskell-cafe@haskell.org/msg100962.html this email from Paul Liu], which ultimately stems from precisely this problem.

I think we've since decided to put left/right back (pulling back on unsaturated type functions), but I need to actually implement it; hence this ticket.

Simon

PS: here's Paul's example
{{{
{-# LANGUAGE GADTs, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts #-}
module Liu where

data Abs env g v where
  Abs :: g (a, env) h v -> Abs env (g (a, env) h v) (a -> v)

class Eval g env h v where
  eval :: env -> g env h v -> v

evalAbs :: Eval g2 (a2, env) h2 v2 
   	=> env 
   	-> Abs env (g2 (a2, env) h2 v2) (a2->v2) 
   	-> (a2->v2)
evalAbs env (Abs e) x 
  = eval (x, env) e    -- e :: g (a,env) h v
}}}
"	feature request	closed	normal		Compiler	7.4.2	fixed		dimitris@… sweirich@… goldfire dreixel adam.gundry@…	Unknown/Multiple	Unknown/Multiple	None/Unknown	Unknown	gadt/T7205