Skip to content

Using a dummy typechecker plugin causes an ambiguity check error

The following variation on [[GhcFile(testsuite/tests/typecheck/should_compile/T10009.hs)]] compiles cleanly:

{-# 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 }
Edited by jme
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information