[GHC] #15192: Refactor of Coercion

[GHC]

#15192: Refactor of Coercion
-------------------------------------+-------------------------------------
        Reporter:  ningning          |                Owner:  ningning
            Type:  task              |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):  Phab:D4747
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Ningning, let me check my understanding

 * In HEAD we have `GRefl` but not `CoherenceCo`

 * In EXPERIMENT you added `CoherenceCo` and used it.

 * You found that EXPERIMENT allocated up to 2.5% less.

 Right so far?

 What are the costs of EXPERIMENT?

 * The extra constructor in Coercion, and extra cases in free-vars,
 substitution, pretty-printing etc.

 * Extra stuff in `OptCoercion`, I assume.  This is already a very tricky
 module, so may be the biggest cost.

 Is that all?

 Other thoughts

 * I recall that `CoerherenceCo` was biased to the laft. One could add a
 right-biased version too -- would that help even more?

 * Are you implicitly advocating adding `CoherenceCo` not for
 expressiveness but for efficiency?  And if so, are there any other
 combinations of coercions that we could play a similar game with?

 * I've noticed (in `tc_trace` printing) that we build a LOT of Refl
 coercions.  Yet the `isGReflCo` case obviously doesn't fire, perhaps
 because the coercion hasn't been zonked.  Yet in fact `zonkTcType`
 ''does'' zonk coercions, so I'm a bit puzzled about why we get quite so
 many of them.  There might be some low-hanging fruit in finding out why.

 * In writing that comment I ''also'' realised that when zonking a type
 (with `zonkTcType`) we fully zonk all the coercions it mentions.  I wonder
 if that is really necessary?  That is, in `zonkTcType` could we simply
 not-zonk any coercions, just doing the latter when we do
 `zonkTcTypeToType`?

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15192#comment:25>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler