[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       |           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