[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
#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