[GHC] #13410: GHC HEAD regression: Template variable unbound in rewrite rule

[GHC]

#13410: GHC HEAD regression: Template variable unbound in rewrite rule
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  simonpj
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:  8.2.1
       Component:  Compiler          |              Version:  8.0.1
      Resolution:                    |             Keywords:  JoinPoints,
                                     |  SpecConstr
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Simon Peyton Jones <simonpj@…>):

 In [changeset:"8674883c137401873fd53a6963acd33af651c2af/ghc"
 8674883c/ghc]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="8674883c137401873fd53a6963acd33af651c2af"
 Allow unbound Refl binders in a RULE

 Trac #13410 was failing because we had a RULE with a binder
    (c :: t~t)
 and the /occurrences/ of c on the LHS were being optimised to Refl,
 leaving a binder that would not be filled in by matching the LHS
 of the rule.

 I flirted with trying to ensure that occurrences (c :: t~t) are
 not optimised to Relf, but that turned out to be fragile; it was
 being done, for good reasons, in multiple places, including
   - TyCoRep.substCoVarBndr
   - Simplify.simplCast
   - Corecion.mkCoVarCo

 So I fixed it in one place by making Rules.matchN deal happily
 with an unbound binder (c :: t~t).  Quite easy.  See "Coercion
 variables" in Note [Unbound RULE binders] in Rules.

 In addition, I needed to make CoreLint be happy with an bound
 RULE binder that is a Relf coercion variable

 In debugging this, I was perplexed that occurrences of a variable
 (c :: t~t) mysteriously turned into Refl.  I found out how it
 was happening, and decided to move it:

 * In TyCoRep.substCoVarBndr, do not substitute Refl for a
   binder (c :: t~t).

 * In mkCoVarCo do not optimise (c :: t~t) to Refl.

 Instead, we do this optimisation in optCoercion (specifically
 opt_co4) where, surprisingly, the optimisation was /not/
 being done.  This has no effect on what programs compile;
 it just moves a relatively-expensive optimisation to optCoercion,
 where it seems more properly to belong.  It's actually not clear
 to me which is really "better", but this way round is less
 surprising.

 One small simplifying refactoring

 * Eliminate TyCoRep.substCoVarBndrCallback, which was only
   called locally.
 }}}

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