Re: [GHC] #11525: Using a dummy typechecker plugin causes an ambiguity check error

2 Feb 2016


      #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

    