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