Opened 3 years ago

Last modified 2 months ago

#11457 new feature request

Run type-checker plugins before GHC's solver

Reported by: gridaphobe Owned by:
Priority: normal Milestone: 8.8.1
Component: Compiler (Type checker) Version: 8.0.1-rc1
Keywords: TypeCheckerPlugins Cc: adamgundry, diatchki, angerman
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Here's an odd use-case for type-checker plugins: rejecting valid programs that the user doesn't like, for example, programs that use a class instance with confusing behavior (like the functor/traversable instances on tuples).

Unfortunately, we can't write such a plugin at the moment because GHC runs its own solver first, and will (I think) discharge any dictionary constraints before the plugin can run. If instead we run the plugins first, a plugin could mark undesired instances as insoluble.

See the discussion at http://mail.haskell.org/pipermail/libraries/2016-January/026602.html for the original motivation.

Thoughts?

Change History (8)

comment:1 Changed 3 years ago by dfeuer

We need to intertwine the various aspects, and I don't know how that works with the plugin infrastructure. For example, if we have (hypothetically)

import Prelude.Extras
{-# SuppressInstance Functor ((,) a) #-}

foo :: (p -> q) -> Lift1 ((,) x) p -> Lift1 ((,) x) q
foo = fmap

GHC will recognize a Functor (Lift1 ((,) x)) constraint. We need the usual constraint solver to run far enough to determine that this requires Functor ((,) x) before we can step in and reject the solution.


Note that the suppression regime has not yet gone far enough for a full-on proposal yet. Some things people might want:

  1. Suppress or warn about an instance unconditionally. This is clearly the simplest case, and covers the immediate demand.
  2. Suppress or warn about an instance if a certain constraint *can* be satisfied. This seems a bit shady, but it may have applications.
  3. Suppress or warn about use of an instance if a certain constraint *cannot* be satisfied. That is, add that constraint to the instance temporarily. This might be desirable if an instance is *implementable* without the given constraint, but doesn't really make *sense* without it.

comment:2 Changed 3 years ago by adamgundry

Indeed, rejecting potentially-solvable constraints would be a bit tricky to do accurately, because of the intertwining of different kinds of constraint solving. It should be easy to run the plugins first and permit them to reject dictionary constraints that have arisen directly from the source, but it's not clear that is very useful because many constraints arise during solving. (Moreover, this would not work for equality constraints, because those are handled eagerly by the unifier.)

I suppose one could imagine an alternative architecture for plugins that gave them each new constraint as GHC generated it, which would be capable of doing this, but would be much more deeply tied into GHC's constraint-solving algorithm.

Another possibility we've considered in the past is making it possible for a plugin to replace GHC's entire constraint solver pipeline. That could be interesting from the point of view of experimenting with alternative constraint-solving algorithms, but I'm not sure how feasible it is.

For this specific feature request, I suspect it would be easier to do it inside GHC itself, by checking for suppression pragmas during instance lookup.

comment:3 in reply to:  2 Changed 3 years ago by gridaphobe

Replying to adamgundry:

It should be easy to run the plugins first and permit them to reject dictionary constraints that have arisen directly from the source, but it's not clear that is very useful because many constraints arise during solving.

Shouldn't plugins get access to the extra constraints as part of the inner loop in solveSimpleWanteds? Oh I see, solveSimples has its own loop that greedily solves the constraints that it can, bummer..

We could change solveSimples to not grab constraints from the work-list directly, but to just solve the constraints it's given. Then any new work-list items would have to go through the whole pipeline, including plugins. I don't know what the performance implications would be though.

But even then, it would still be hard to ensure that our plugin gets to reject the dictionary constraint, what if another plugin runs first and solves it? Hrm..

(Moreover, this would not work for equality constraints, because those are handled eagerly by the unifier.)

Right, but to be fair, I can't think of a reason I, as a user, would want to reject an equality constraint that can be proven.

comment:4 Changed 2 years ago by bgamari

Milestone: 8.0.18.2.1

This bug won't be fixed in 8.0.1; bumping to 8.2.

comment:5 Changed 20 months ago by bgamari

Cc: angerman added
Milestone: 8.2.18.4.1

This won't happen for 8.2.

Angerman, you might be interested in this considering your recent reflections on plugins.

comment:6 Changed 7 months ago by bgamari

Milestone: 8.4.18.6.1

This ticket won't be resolved in 8.4; remilestoning for 8.6. Do holler if you are affected by this or would otherwise like to work on it.

comment:7 Changed 3 months ago by adamgundry

Keywords: TypeCheckerPlugins added; plugin removed

comment:8 Changed 2 months ago by bgamari

Milestone: 8.6.18.8.1

These won't be fixed for 8.6, bumping to 8.8.

Note: See TracTickets for help on using tickets.