[GHC] #15725: Core Lint error: Trans coercion mis-match

[GHC]

#15725: Core Lint error: Trans coercion mis-match
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.8.1
       Component:  Compiler          |              Version:  8.6.1
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #15703            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 It appears that `simplCoercion` is the thing that's producing this ill-
 formed coercion. Here is the input coercion:

 {{{
 Sym (Nth:2
          (Inst (forall (x1 :: Sym (Bug.D:R:Rep1Identity[0]) <a>_N).
                 (Bug.Sing
                    (Sym (Bug.D:R:Rep1Identity[0]) <a>_N)
                    (GRefl nominal x1 (Sym (Bug.D:R:Rep1Identity[0])
 <a>_N)))_R
                 ->_R (Bug.Sing
                         (Sym (Bug.D:R:Rep1Identity[0]) <a>_N)
                         (Sym (Bug.D:R:MethTYPEPar1px[0] <a>_N <x1>_N) ;
 (Bug.Meth
 <*>_N
 (Sym (Bug.D:R:Rep1Identity[0]))
 <a>_N
 (GRefl nominal x1
 (Sym (Bug.D:R:Rep1Identity[0]) <a>_N)))_N))_R) (Sym (GRefl nominal
 (Bug.From1
 x)
 (Sym (Sym (Bug.D:R:Rep1Identity[0]) <a>_N))))))
 }}}

 And here is the output coercion:

 {{{
 Nth:2
     ((Bug.Sing
         (Bug.D:R:Rep1Identity[0] <a>_N)
         (Sym (GRefl nominal (Bug.From1 x)
                   ((Bug.D:R:Rep1Identity[0] <a>_N ; Sym (Sym
 (Bug.D:R:Rep1Identity[0]) <a>_N)) ; Sym (Bug.D:R:Rep1Identity[0])
 <a>_N))))_R
      ->_R (Bug.Sing
              (Bug.D:R:Rep1Identity[0] <a>_N)
              ((Bug.Meth
                  <*>_N
                  (Bug.D:R:Rep1Identity[0])
                  <a>_N
                  (Sym (GRefl nominal (Bug.From1 x)
                            ((Bug.D:R:Rep1Identity[0] <a>_N ; Sym (Sym
 (Bug.D:R:Rep1Identity[0]) <a>_N)) ; Sym (Bug.D:R:Rep1Identity[0])
 <a>_N))))_N ; Bug.D:R:MethTYPEPar1px[0]
 <a>_N
 (GRefl nominal (Bug.From1
 x)
 (Bug.D:R:Rep1Identity[0] <a>_N ; Sym (Sym (Bug.D:R:Rep1Identity[0])
 <a>_N)))))_R)
 }}}

 I haven't dug deeper than that.

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