[commit: ghc] master: Exploit the invariant for AxInstCo to simplify coercionKind (2ec39c7)

[Simon Peyton Jones]

Repository : ssh://darcs.haskell.org//srv/darcs/ghc

On branch  : master

http://hackage.haskell.org/trac/ghc/changeset/2ec39c76b9816f76f60076fb52c8038035cd1f7b

>---------------------------------------------------------------

commit 2ec39c76b9816f76f60076fb52c8038035cd1f7b
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Tue Jan 22 16:57:35 2013 +0000

    Exploit the invariant for AxInstCo to simplify coercionKind

>---------------------------------------------------------------

 compiler/types/Coercion.lhs |   20 +++++++++++---------
 1 files changed, 11 insertions(+), 9 deletions(-)

diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs
index 83f31af..abaf7dd 100644
--- a/compiler/types/Coercion.lhs
+++ b/compiler/types/Coercion.lhs
@@ -142,10 +142,13 @@ data Coercion
 
   -- These are special
   | CoVarCo CoVar
-  | AxiomInstCo (CoAxiom Branched) Int [Coercion]
-     -- The coercion arguments always *precisely* saturate arity of CoAxiom.
-     -- See [Coercion axioms applied to coercions]
+  | AxiomInstCo (CoAxiom Branched) BranchIndex [Coercion]
      -- See also [CoAxiom index]
+     -- The coercion arguments always *precisely* saturate 
+     -- arity of (that branch of) the CoAxiom.  If there are
+     -- any left over, we use AppCo.  See 
+     -- See [Coercion axioms applied to coercions]
+
   | UnsafeCo Type Type
   | SymCo Coercion
   | TransCo Coercion Coercion
@@ -1162,12 +1165,11 @@ coercionKind co = go co
     go (CoVarCo cv)         = toPair $ coVarKind cv
     go (AxiomInstCo ax ind cos)
       | CoAxBranch { cab_tvs = tvs, cab_lhs = lhs, cab_rhs = rhs } <- coAxiomNthBranch ax ind
-      , (cos1, cos2) <- splitAtList tvs cos
-      , Pair tys1 tys2 <- sequenceA (map go cos1)
-      = mkAppTys 
-        <$> Pair (substTyWith tvs tys1 (mkTyConApp (coAxiomTyCon ax) lhs))
-                 (substTyWith tvs tys2 rhs)
-        <*> sequenceA (map go cos2)
+      , Pair tys1 tys2 <- sequenceA (map go cos)
+      = ASSERT( cos `equalLength` tvs )  -- Invariant of AxiomInstCo: cos should 
+                                         -- exactly saturate the axiom branch
+        Pair (substTyWith tvs tys1 (mkTyConApp (coAxiomTyCon ax) lhs))
+             (substTyWith tvs tys2 rhs)
     go (UnsafeCo ty1 ty2)   = Pair ty1 ty2
     go (SymCo co)           = swap $ go co
     go (TransCo co1 co2)    = Pair (pFst $ go co1) (pSnd $ go co2)