[GHC] #15639: Surprising failure combining QuantifiedConstraints with Coercible

[GHC]

#15639: Surprising failure combining QuantifiedConstraints with Coercible
-------------------------------------+-------------------------------------
        Reporter:  dfeuer            |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.5
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by dfeuer):

 `-ddump-cs-trace` gives

 {{{
 Step 1[l:1,d:1] Kept as inert:
     [WD] hole{co_a11c} {1}:: t_ax2[tau:0]
                              GHC.Prim.~# 'GHC.Types.LiftedRep
 simpl_loop iteration=0 (no new given superclasses = True, 1 simples to
 solve)
 Step 2[l:0,d:1] Solved by unification:
     [WD] hole{co_a11c} {1}:: t_ax2[tau:0]
                              GHC.Prim.~# 'GHC.Types.LiftedRep
 Constraint solver steps = 2
 Step 1[l:2,d:0] Given forall-constraint:
     [G] df_a11t {0}:: forall a b. Coercible (Yeah a) (Yeah b)
 Step 2[l:2,d:0] Decomposed TyConApp:
     [WD] hole{co_a11z} {0}:: Coercion a_a11w[tau:2] b_a11x[tau:2]
                              GHC.Prim.~# r_a11r[tau:1]
 Step 3[l:2,d:0] Kept as inert:
     [WD] hole{co_a11F} {0}:: b_a11x[tau:2]
                              GHC.Prim.~# [Yeah b_a11l[sk:1]]
 Kick out, tv = k_a11v[tau:2]
   n-kicked = 1
   kicked_out = WL {Eqs = [WD] hole{co_a11F} {0}:: b_a11x[tau:2]
                                                   GHC.Prim.~# [Yeah
 b_a11l[sk:1]] (CIrredCan(sol))}
   Residual inerts = {Given instances = [G] df_a11t {0}:: forall a b.
                                                          Coercible (Yeah
 a) (Yeah b)
                      Unsolved goals = 0}
 Step 4[l:2,d:0] Solved by unification (1 kicked out):
     [D] _ {0}:: k_a11v[tau:2] GHC.Prim.~# *
 Step 5[l:2,d:0] Solved by unification:
     [WD] hole{co_a11F} {0}:: b_a11x[tau:2]
                              GHC.Prim.~# [Yeah b_a11l[sk:1]]
 Step 6[l:2,d:0] Solved by unification:
     [WD] hole{co_a11E} {0}:: a_a11w[tau:2]
                              GHC.Prim.~# [Yeah a_a11k[sk:1]]
 Step 7[l:2,d:0] Solved by reflexivity:
     [WD] hole{co_a11D} {0}:: k_a11v[tau:2] GHC.Prim.~# *
 Step 8[l:2,d:0] Dict/Top (solved wanted):
     [WD] $dCoercible_a11y {0}:: Coercible
                                   [Yeah a_a11k[sk:1]] [Yeah b_a11l[sk:1]]
 Step 9[l:2,d:1] Decomposed TyConApp:
     [WD] hole{co_a11G} {1}:: [Yeah a_a11k[sk:1]]
                              ~R# [Yeah b_a11l[sk:1]]
 Step 10[l:2,d:1] Decomposed TyConApp:
     [WD] hole{co_a11H} {1}:: Yeah a_a11k[sk:1] ~R# Yeah b_a11l[sk:1]
 Step 11[l:2,d:1] Kept as inert:
     [WD] hole{co_a11I} {1}:: a_a11k[sk:1] ~R# b_a11l[sk:1]
 Step 12[l:2,d:0] Given forall-constraint:
     [G] df_a11J {0}:: forall a b. Yeah a ~R# Yeah b
 simpl_loop iteration=0 (no new given superclasses = False, 1 simples to
 solve)
 Step 13[l:2,d:1] Kept as inert:
     [WD] hole{co_a11I} {1}:: a_a11k[sk:1] ~R# b_a11l[sk:1]
 Constraint solver steps = 13
 }}}

 I don't know quite how to read this, but I'd have expected

 {{{
 Step 10[l:2,d:1] Decomposed TyConApp:
     [WD] hole{co_a11H} {1}:: Yeah a_a11k[sk:1] ~R# Yeah b_a11l[sk:1]
 }}}

 to interact with

 {{{
 Step 12[l:2,d:0] Given forall-constraint:
     [G] df_a11J {0}:: forall a b. Yeah a ~R# Yeah b
 }}}

 and resolve.

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