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