[GHC] #11525: Using a dummy typechecker plugin causes an ambiguity check error
#11525: Using a dummy typechecker plugin causes an ambiguity check error -------------------------------------+------------------------------------- Reporter: jme | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1-rc1 (Type checker) | 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: -------------------------------------+------------------------------------- The following variation on [[GhcFile(testsuite/tests/typecheck/should_compile/T10009.hs)]] compiles cleanly: {{{#!hs {-# LANGUAGE TypeFamilies, ScopedTypeVariables #-} {-# OPTIONS_GHC -fno-warn-redundant-constraints #-} module T10009WithClass where type family F a type family UnF a class (UnF (F b) ~ b) => C b where f :: F b -> () g :: forall a. (C a) => a -> () g _ = f (undefined :: F a) }}} But compiling it with the dummy typechecker plugin [[GhcFile(testsuite/tests/typecheck/should_compile/T11462_Plugin.hs)]] yields {{{ $ ghc -dynamic -c T11462_Plugin.hs $ ghc -fplugin=T11462_Plugin -dynamic -c T10009WithClass.hs T10009WithClass.hs:10:5: error: - Could not deduce: F b0 ~ F b from the context: C b bound by the type signature for: f :: C b => F b -> () at T10009WithClass.hs:10:5-18 NB: 'F' is a type function, and may not be injective The type variable 'b0' is ambiguous Expected type: F b -> () Actual type: F b0 -> () - In the ambiguity check for 'f' To defer the ambiguity check to use sites, enable AllowAmbiguousTypes When checking the class method: f :: forall b. C b => F b -> () In the class declaration for 'C' }}} Superficially, the problem is that the presence of the plugin causes `runTcPluginsWanted` to zonk the pending superclass constraint, changing it to a `CNonCanonical`. This in turn prevents `solveWanteds` from making any further progress (which ultimately leads to the error): {{{ getUnsolvedInerts tv eqs = {[W] hole{aIO} :: s_aIL[fuv:2] GHC.Prim.~# fsk_aIC[fsk] (CTyEqCan)} fun eqs = {[W] hole{aIM} :: F b_aIu[tau:3] GHC.Prim.~# s_aIL[fuv:2] (CFunEqCan)} insols = {} others = {[W] $dC_aIv :: C b_aIu[tau:3] (CDictCan(psc))} <===== BEFORE plugin implics = {} Unflattening {Funeqs = [W] hole{aIM} :: F b_aIu[tau:3] GHC.Prim.~# s_aIL[fuv:2] (CFunEqCan) Tv eqs = [W] hole{aIO} :: s_aIL[fuv:2] GHC.Prim.~# fsk_aIC[fsk] (CTyEqCan)} Filling coercion hole aIM := <F b_aIu[tau:3]>_N unflattenFmv s_aIL[fuv:2] := F b_aIu[tau:3] writeMetaTyVar s_aIL[fuv:2] :: * := F b_aIu[tau:3] Unflattening 1 {} Unflattening 2 {[W] hole{aIO} :: s_aIL[fuv:2] GHC.Prim.~# fsk_aIC[fsk] (CTyEqCan)} Unflattening 3 {} Unflattening done {[W] hole{aIO} :: s_aIL[fuv:2] GHC.Prim.~# fsk_aIC[fsk] (CNonCanonical)} zonkSimples done: {[W] hole{aIO} :: F b_aIu[tau:3] GHC.Prim.~# F b_aIs[sk] (CNonCanonical)} zonkSimples done: {[W] $dC_aIv :: C b_aIu[tau:3] (CNonCanonical), <===== AFTER plugin [W] hole{aIO} :: F b_aIu[tau:3] GHC.Prim.~# F b_aIs[sk] (CNonCanonical)} solveSimples end } iterations = 1 residual = WC {wc_simple = [W] $dC_aIv :: C b_aIu[tau:3] (CNonCanonical) [W] hole{aIO} :: F b_aIu[tau:3] GHC.Prim.~# F b_aIs[sk] (CNonCanonical)} solveWanteds } }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11525> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11525: Using a dummy typechecker plugin causes an ambiguity check error -------------------------------------+------------------------------------- Reporter: jme | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1-rc1 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: | -------------------------------------+------------------------------------- Description changed by jme: @@ -61,1 +61,0 @@ - plugin @@ -83,1 +82,0 @@ - plugin New description: The following variation on [[GhcFile(testsuite/tests/typecheck/should_compile/T10009.hs)]] compiles cleanly: {{{#!hs {-# LANGUAGE TypeFamilies, ScopedTypeVariables #-} {-# OPTIONS_GHC -fno-warn-redundant-constraints #-} module T10009WithClass where type family F a type family UnF a class (UnF (F b) ~ b) => C b where f :: F b -> () g :: forall a. (C a) => a -> () g _ = f (undefined :: F a) }}} But compiling it with the dummy typechecker plugin [[GhcFile(testsuite/tests/typecheck/should_compile/T11462_Plugin.hs)]] yields {{{ $ ghc -dynamic -c T11462_Plugin.hs $ ghc -fplugin=T11462_Plugin -dynamic -c T10009WithClass.hs T10009WithClass.hs:10:5: error: - Could not deduce: F b0 ~ F b from the context: C b bound by the type signature for: f :: C b => F b -> () at T10009WithClass.hs:10:5-18 NB: 'F' is a type function, and may not be injective The type variable 'b0' is ambiguous Expected type: F b -> () Actual type: F b0 -> () - In the ambiguity check for 'f' To defer the ambiguity check to use sites, enable AllowAmbiguousTypes When checking the class method: f :: forall b. C b => F b -> () In the class declaration for 'C' }}} Superficially, the problem is that the presence of the plugin causes `runTcPluginsWanted` to zonk the pending superclass constraint, changing it to a `CNonCanonical`. This in turn prevents `solveWanteds` from making any further progress (which ultimately leads to the error): {{{ getUnsolvedInerts tv eqs = {[W] hole{aIO} :: s_aIL[fuv:2] GHC.Prim.~# fsk_aIC[fsk] (CTyEqCan)} fun eqs = {[W] hole{aIM} :: F b_aIu[tau:3] GHC.Prim.~# s_aIL[fuv:2] (CFunEqCan)} insols = {} others = {[W] $dC_aIv :: C b_aIu[tau:3] (CDictCan(psc))} <===== BEFORE implics = {} Unflattening {Funeqs = [W] hole{aIM} :: F b_aIu[tau:3] GHC.Prim.~# s_aIL[fuv:2] (CFunEqCan) Tv eqs = [W] hole{aIO} :: s_aIL[fuv:2] GHC.Prim.~# fsk_aIC[fsk] (CTyEqCan)} Filling coercion hole aIM := <F b_aIu[tau:3]>_N unflattenFmv s_aIL[fuv:2] := F b_aIu[tau:3] writeMetaTyVar s_aIL[fuv:2] :: * := F b_aIu[tau:3] Unflattening 1 {} Unflattening 2 {[W] hole{aIO} :: s_aIL[fuv:2] GHC.Prim.~# fsk_aIC[fsk] (CTyEqCan)} Unflattening 3 {} Unflattening done {[W] hole{aIO} :: s_aIL[fuv:2] GHC.Prim.~# fsk_aIC[fsk] (CNonCanonical)} zonkSimples done: {[W] hole{aIO} :: F b_aIu[tau:3] GHC.Prim.~# F b_aIs[sk] (CNonCanonical)} zonkSimples done: {[W] $dC_aIv :: C b_aIu[tau:3] (CNonCanonical), <===== AFTER [W] hole{aIO} :: F b_aIu[tau:3] GHC.Prim.~# F b_aIs[sk] (CNonCanonical)} solveSimples end } iterations = 1 residual = WC {wc_simple = [W] $dC_aIv :: C b_aIu[tau:3] (CNonCanonical) [W] hole{aIO} :: F b_aIu[tau:3] GHC.Prim.~# F b_aIs[sk] (CNonCanonical)} solveWanteds } }}} -- -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11525#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11525: Using a dummy typechecker plugin causes an ambiguity check error -------------------------------------+------------------------------------- Reporter: jme | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1-rc1 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 darchon): I've just ran into this bug, did you ever find a work-around? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11525#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11525: Using a dummy typechecker plugin causes an ambiguity check error -------------------------------------+------------------------------------- Reporter: jme | Owner: Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1-rc1 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: | -------------------------------------+------------------------------------- Changes (by darchon): * milestone: => 8.2.1 Comment: As I (`christiaanb` on IRC) have several type-checker plugins released on Hackage, I would like to see a fix for this included in the GHC 8.2.1 release. I've already asked Adam Gundry for some guidance in helping me fix it. Although I surely wouldn't mind if someone with more familiarity with the affected part of the codebase could work out a fix for this bug instead ;-) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11525#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11525: Using a dummy typechecker plugin causes an ambiguity check error -------------------------------------+------------------------------------- Reporter: jme | Owner: Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Resolution: | UndecidableSuperClasses, plugin 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: | -------------------------------------+------------------------------------- Changes (by adamgundry): * cc: adamgundry, simonpj (added) * keywords: => UndecidableSuperClasses, plugin Comment: Thanks for pointing me to this bug. The problem would appear to be the `UndecidableSuperClasses` changes in 6eabb6ddb7c53784792ee26b1e0657bde7eee7fb, which introduced a new `expandSuperClasses` step after the `solveSimpleWanteds` loop. This is the step that looks for `CDictCan`, and hence fails to expand the constraint because the plugin-induced zonking has turned it into a `CNonCanonical` instead. I think the right way to fix this is to change `zonkCt` so that it preserves `CDictCan`, much as it already preserves `CHoleCan`. We want to zonk before running the plugins, as otherwise the plugins will have to expand mutable type variables themselves. I suspect that we shouldn't modify `expandSuperClasses` to look for `CNonCanoical` dictionaries, because it passes around information in the `cc_pend_sc` field of `CDictCan`. The code has changed quite a bit since I last looked at it, however, so it might be worth checking with someone more knowledgeable than me (simonpj?) if this makes sense. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11525#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11525: Using a dummy typechecker plugin causes an ambiguity check error -------------------------------------+------------------------------------- Reporter: jme | Owner: Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Resolution: | UndecidableSuperClasses, plugin 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 simonpj): Thank you Adam. I'm deeply swamped all this week and most of next. Could you articulate in a bit more detail, starting from zero, what the problem is, and why zonking `CDictCan` differently would help? Then I'll try to respond. Simon -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11525#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11525: Using a dummy typechecker plugin causes an ambiguity check error -------------------------------------+------------------------------------- Reporter: jme | Owner: Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Resolution: | UndecidableSuperClasses, plugin 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 adamgundry): Okay, let me try to summarise: 1. When a type-checker plugin is in use, we zonk the constraints before calling the plugin. Thus plugins don't need to worry about doing their own zonking. 2. Zonking a `CDictCan` constraint (or indeed anything other than a `CHoleCan`) turns it into a `CNonCanonical`. Presumably this is because zonking may not preserve the invariants of all the canonical constraints, so they might need to be re-canonicalized if they are looked at again later. 3. The `expandSuperClasses` step, which runs after the simple wanted and plugin loop, looks for `CDictCan`s. If a plugin is in use, 1 and 2 mean that it doesn't find any, and hence fails to expand superclasses. This leads to the solving failure reported in this ticket. If we can make `zonkCt` preserve `CDictCan` rather than turning it into `CNonCanonical`, then `expandSuperClasses` should just work even in the presence of plugins. However, it isn't completely obvious to me whether the invariants of `CDictCan` (e.g. the fact that `cc_tyargs` is "function- free") will still hold after zonking. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11525#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11525: Using a dummy typechecker plugin causes an ambiguity check error -------------------------------------+------------------------------------- Reporter: jme | Owner: Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Resolution: | UndecidableSuperClasses, plugin 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 simonpj): Oh, (3) is terrible! It's find just to elaborate `zonkCt`. Constraints are always re-flattened etc even if they come in as `CDictCan`. Only canonical constraints that are actually ''in the inert set'' carry all the guarantees. That point should be more carefully documented, I agree. It's a bit more code to do this (which is, I think, why `zonkCt` currently always returns a `CNonCanonical`), so please include a Note to explain. Also * `CTyEqCan`: flattening the LHS might not give a type variable; if not, return a `CNonCanonical`. * `CFunEqCan`: you could do the same for the `cc_fsk` field, but I don't think `zonkCt` should ever encounter a `CFunEqCan`, because the latter are removed by `TcFlatten.unflatten`. So you could just crash. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11525#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11525: Using a dummy typechecker plugin causes an ambiguity check error -------------------------------------+------------------------------------- Reporter: jme | Owner: darchon Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Resolution: | UndecidableSuperClasses, plugin Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: T11525 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): D3105 Wiki Page: | -------------------------------------+------------------------------------- Changes (by darchon): * owner: => darchon * testcase: => T11525 * differential: => D3105 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11525#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11525: Using a dummy typechecker plugin causes an ambiguity check error -------------------------------------+------------------------------------- Reporter: jme | Owner: darchon Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Resolution: | UndecidableSuperClasses, plugin Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: T11525 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | https://phabricator.haskell.org/D3105 -------------------------------------+------------------------------------- Changes (by darchon): * differential: D3105 => https://phabricator.haskell.org/D3105 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11525#comment:9> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11525: Using a dummy typechecker plugin causes an ambiguity check error -------------------------------------+------------------------------------- Reporter: jme | Owner: darchon Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Resolution: | UndecidableSuperClasses, plugin Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: T11525 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D3105 Wiki Page: | -------------------------------------+------------------------------------- Changes (by mpickering): * differential: https://phabricator.haskell.org/D3105 => Phab:D3105 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11525#comment:10> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11525: Using a dummy typechecker plugin causes an ambiguity check error -------------------------------------+------------------------------------- Reporter: jme | Owner: darchon Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Resolution: | UndecidableSuperClasses, plugin Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: T11525 Blocked By: | Blocking: Related Tickets: #12780 | Differential Rev(s): Phab:D3105 Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * related: => #12780 Comment: When this is done, revisit #12780 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11525#comment:11> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11525: Using a dummy typechecker plugin causes an ambiguity check error -------------------------------------+------------------------------------- Reporter: jme | Owner: darchon Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Resolution: | UndecidableSuperClasses, plugin Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: T11525 Blocked By: | Blocking: Related Tickets: #12780 | Differential Rev(s): Phab:D3105 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Ben Gamari <ben@…>): In [changeset:"07292e958cb0c08705d9a694f09d9621058b16e6/ghc" 07292e95/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="07292e958cb0c08705d9a694f09d9621058b16e6" zonkCt tries to maintain the canonical form of a Ct. For example, - a CDictCan should stay a CDictCan; - a CTyEqCan should stay a CTyEqCan (if the LHS stays as a variable.). - a CHoleCan should stay a CHoleCan Why? For CDicteqCan see Trac #11525. Test Plan: Validate Reviewers: austin, adamgundry, simonpj, goldfire, bgamari Reviewed By: simonpj, bgamari Subscribers: thomie Differential Revision: https://phabricator.haskell.org/D3105 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11525#comment:12> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11525: Using a dummy typechecker plugin causes an ambiguity check error -------------------------------------+------------------------------------- Reporter: jme | Owner: darchon Type: bug | Status: merge Priority: normal | Milestone: 8.0.3 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Resolution: | UndecidableSuperClasses, plugin Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: T11525 Blocked By: | Blocking: Related Tickets: #12780 | Differential Rev(s): Phab:D3105 Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: new => merge * milestone: 8.2.1 => 8.0.3 Comment: If we do a 8.0.3 it would likely be worthwhile trying to backport this since it's a regression. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11525#comment:13> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11525: Using a dummy typechecker plugin causes an ambiguity check error -------------------------------------+------------------------------------- Reporter: jme | Owner: darchon Type: bug | Status: closed Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Resolution: fixed | UndecidableSuperClasses, plugin Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: T11525 Blocked By: | Blocking: Related Tickets: #12780 | Differential Rev(s): Phab:D3105 Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: merge => closed * resolution: => fixed -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11525#comment:15> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11525: Using a dummy typechecker plugin causes an ambiguity check error -------------------------------------+------------------------------------- Reporter: jme | Owner: darchon Type: bug | Status: closed Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Resolution: fixed | UndecidableSuperClasses, | TypeCheckerPlugins Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: T11525 Blocked By: | Blocking: Related Tickets: #12780 | Differential Rev(s): Phab:D3105 Wiki Page: | -------------------------------------+------------------------------------- Changes (by adamgundry): * keywords: UndecidableSuperClasses, plugin => UndecidableSuperClasses, TypeCheckerPlugins -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11525#comment:16> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC