Opened 3 years ago

Closed 18 months ago

Last modified 3 months ago

#11525 closed bug (fixed)

Using a dummy typechecker plugin causes an ambiguity check error

Reported by: jme Owned by: darchon
Priority: normal Milestone: 8.2.1
Component: Compiler (Type checker) Version: 8.0.1-rc1
Keywords: UndecidableSuperClasses, TypeCheckerPlugins Cc: adamgundry, simonpj
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: T11525
Blocked By: Blocking:
Related Tickets: #12780 Differential Rev(s): Phab:D3105
Wiki Page:

Description (last modified by jme)

The following variation on 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 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 }

Change History (16)

comment:1 Changed 3 years ago by jme

Description: modified (diff)

comment:2 Changed 19 months ago by darchon

I've just ran into this bug, did you ever find a work-around?

comment:3 Changed 19 months ago by darchon

Milestone: 8.2.1

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 ;-)

comment:4 Changed 19 months ago by adamgundry

Cc: adamgundry simonpj added
Keywords: UndecidableSuperClasses plugin added

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.

comment:5 Changed 19 months ago 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

comment:6 Changed 19 months ago 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.
  1. 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.
  1. The expandSuperClasses step, which runs after the simple wanted and plugin loop, looks for CDictCans. 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.

comment:7 Changed 19 months ago 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.

comment:8 Changed 18 months ago by darchon

Differential Rev(s): D3105
Owner: set to darchon
Test Case: T11525

comment:9 Changed 18 months ago by darchon

Differential Rev(s): D3105https://phabricator.haskell.org/D3105

comment:10 Changed 18 months ago by mpickering

Differential Rev(s): https://phabricator.haskell.org/D3105Phab:D3105

comment:11 Changed 18 months ago by simonpj

When this is done, revisit #12780

comment:12 Changed 18 months ago by Ben Gamari <ben@…>

In 07292e95/ghc:

zonkCt tries to maintain the canonical form of a Ct.

For example,
 - a CDictCan should stay a CDictCan;
 - a CTyEqCan should stay a CTyEqCan (if the LHS stays as a variable.).
 - a CHoleCan should stay a CHoleCan

Why?  For CDicteqCan see Trac #11525.

Test Plan: Validate

Reviewers: austin, adamgundry, simonpj, goldfire, bgamari

Reviewed By: simonpj, bgamari

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D3105

comment:13 Changed 18 months ago by bgamari

Milestone: 8.2.18.0.3
Status: newmerge

If we do a 8.0.3 it would likely be worthwhile trying to backport this since it's a regression.

comment:14 Changed 18 months ago by bgamari

Milestone: 8.0.38.2.1

At this point it is rather unlikely that there will be an 8.0.3. Re-milestoning.

comment:15 Changed 18 months ago by bgamari

Resolution: fixed
Status: mergeclosed

comment:16 Changed 3 months ago by adamgundry

Keywords: TypeCheckerPlugins added; plugin removed
Note: See TracTickets for help on using tickets.