#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