[GHC] #11408: Delicate solve order
#11408: Delicate solve order -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Should we successfully infer a type for `f`: {{{ f x = [h x, [x]] }}} assuming `h :: forall b. F b -> b`? Assuming `(x::alpha)` and we instantiate `h` at `beta`, we get the constraints {{{ (1) beta ~ [alpha] from the list [h x, [x]] (2) alpha ~ F beta from the call of h }}} Now if we happen to unify the constraint (1) first, `beta := [alpha`], then we successfully infer {{{ f :: forall a. (a ~ F [a]) => a -> [[a]] }}} But if we unify the constraint (2) first, `alpha := F beta`, we get {{{ f :: forall b. (b ~ [F b]) => F b -> [[F b]] }}} which is ambiguous. Eeek! This actually shows up in type inference for `indexed- types/should_compile/IndTypesPerfMerge`, where the function `merge` has (a slightly more complicated form of) this delicately-balanced situation. But see `Note [Orientation of equalities with fmvs]` in `TcFlatten` for why we don't defer solving (2). -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11408> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11408: Delicate solve order -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones <simonpj@…>): In [changeset:"9308c736d43b92bf8634babf565048e66e071bd8/ghc" 9308c736/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="9308c736d43b92bf8634babf565048e66e071bd8" Fix a number of subtle solver bugs As a result of some other unrelated changes I found that IndTypesPerf was failing, and opened Trac #11408. There's a test in indexed-types/should-compile/T11408. The bug was that a type like forall t. (MT (UL t) (UR t) ~ t) => UL t -> UR t -> Int is in fact unambiguous, but it's a bit subtle to prove that it is unambiguous. In investigating, Dimitrios and I found several subtle bugs in the constraint solver, fixed by this patch * canRewrite was missing a Derived/Derived case. This was lost by accident in Richard's big kind-equality patch. * Interact.interactTyVarEq would discard [D] a ~ ty if there was a [W] a ~ ty in the inert set. But that is wrong because the former can rewrite things that the latter cannot. Fix: a new function eqCanDischarge * In TcSMonad.addInertEq, the process was outright wrong for a Given/Wanted in the (GWModel) case. We were adding a new Derived without kicking out things that it could rewrite. Now the code is simpler (no special GWModel case), and works correctly. * The special case in kickOutRewritable for [W] fsk ~ ty, turns out not to be needed. (We emit a [D] fsk ~ ty which will do the job. I improved comments and documentation, esp in TcSMonad. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11408#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11408: Delicate solve order -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: indexed- | types/should_compile/T11408 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * testcase: => indexed-types/should_compile/T11408 * resolution: => fixed Old description:
Should we successfully infer a type for `f`: {{{ f x = [h x, [x]] }}} assuming `h :: forall b. F b -> b`?
Assuming `(x::alpha)` and we instantiate `h` at `beta`, we get the constraints {{{ (1) beta ~ [alpha] from the list [h x, [x]] (2) alpha ~ F beta from the call of h }}} Now if we happen to unify the constraint (1) first, `beta := [alpha`], then we successfully infer {{{ f :: forall a. (a ~ F [a]) => a -> [[a]] }}} But if we unify the constraint (2) first, `alpha := F beta`, we get {{{ f :: forall b. (b ~ [F b]) => F b -> [[F b]] }}} which is ambiguous.
Eeek! This actually shows up in type inference for `indexed- types/should_compile/IndTypesPerfMerge`, where the function `merge` has (a slightly more complicated form of) this delicately-balanced situation.
But see `Note [Orientation of equalities with fmvs]` in `TcFlatten` for why we don't defer solving (2).
New description: Should we successfully infer a type for `f`: {{{ f x = [h x, [x]] }}} assuming `h :: forall b. F b -> b`? Assuming `(x::alpha)` and we instantiate `h` at `beta`, we get the constraints {{{ (1) beta ~ [alpha] from the list [h x, [x]] (2) alpha ~ F beta from the call of h }}} Now if we happen to unify the constraint (1) first, `beta := [alpha`], then we successfully infer {{{ f :: forall a. (a ~ F [a]) => a -> [[a]] }}} But if we unify the constraint (2) first, `alpha := F beta`, we get {{{ f :: forall b. (b ~ [F b]) => F b -> [[F b]] }}} which looks ambiguous. It isn't ambiguous, in fact, but the solver has to work hard to prove it. It actually succeeds here, but in the more complicated example in `indexed-types/should_compile/IndTypesPerfMerge`, it didn't. There the function `merge` has (a slightly more complicated form of) this delicately-balanced situation. But see `Note [Orientation of equalities with fmvs]` in `TcFlatten` for why we don't defer solving (2). -- -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11408#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11408: Delicate solve order -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: merge Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: indexed- | types/should_compile/T11408 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: closed => merge -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11408#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11408: Delicate solve order -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: indexed- | types/should_compile/T11408 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: merge => closed Comment: This was merged to `ghc-8.0` as 9f466c8841c7ddda84951c9e3470540d25d0bfdb. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11408#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11408: Delicate solve order -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: closed Priority: normal | Milestone: 8.0.1 Component: Compiler | Version: 7.10.3 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: indexed- | types/should_compile/T11408 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * milestone: => 8.0.1 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11408#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC