Opened 4 years ago

Closed 4 years ago

Last modified 4 years ago

#7205 closed feature request (fixed)

Re-introduce left/right coercion decomposition

Reported by: simonpj Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.4.2
Keywords: Cc: dimitris@…, sweirich@…, goldfire, dreixel, adam.gundry@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: gadt/T7205
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


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

    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 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.


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

Change History (7)

comment:1 Changed 4 years ago by simonpj

Cc: dimitris@… sweirich@… goldfire dreixel added

comment:2 Changed 4 years ago by adamgundry

Cc: adam.gundry@… added

comment:3 Changed 4 years ago by guest

see also #5591

comment:4 Changed 4 years ago by simonpj@…

commit af7cc9953217d74e88d4d21512e957edd8e97ec9

Author: Simon Peyton Jones <>
Date:   Mon Sep 17 11:34:28 2012 +0100

    Implement 'left' and 'right' coercions
    This patch finally adds 'left' and 'right' coercions back into
    GHC.  Trac #7205 gives the details.
    The main change is to add a new constructor to Coercion:
      data Coercion
        = ...
        | NthCo  Int         Coercion     -- OLD, still there
        | LRCo   LeftOrRight Coercion     -- NEW
      data LeftOrRight = CLeft | CRight
      * Similar change to TcCoercion
      * Use LRCo when decomposing AppTys
      * Coercion optimisation needs to handle left/right
    The rest is just knock-on effects.

 compiler/coreSyn/CoreLint.lhs        |   13 ++++++++
 compiler/coreSyn/ExternalCore.lhs    |    3 ++
 compiler/coreSyn/MkExternalCore.lhs  |    5 +++
 compiler/coreSyn/PprExternalCore.lhs |    4 ++
 compiler/coreSyn/TrieMap.lhs         |   22 ++++++++++---
 compiler/deSugar/DsBinds.lhs         |    1 +
 compiler/iface/BinIface.hs           |   14 ++++++++-
 compiler/iface/IfaceType.lhs         |    5 ++-
 compiler/iface/TcIface.lhs           |    1 +
 compiler/typecheck/TcCanonical.lhs   |   14 ++-------
 compiler/typecheck/TcEvidence.lhs    |   14 +++++++--
 compiler/typecheck/TcHsSyn.lhs       |    1 +
 compiler/typecheck/TcType.lhs        |    1 +
 compiler/types/Coercion.lhs          |   31 +++++++++++++++++--
 compiler/types/OptCoercion.lhs       |   56 ++++++++++++++++++++++++++++-----
 15 files changed, 152 insertions(+), 33 deletions(-)

comment:5 Changed 4 years ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: gadt/T7205

Done at last.


comment:6 Changed 4 years ago by morabbin

See #6108; is this related?

comment:7 Changed 4 years ago by morabbin

That should #6018; apologies.

Note: See TracTickets for help on using tickets.