Coercions from plugins cannot be stopped from floating out

Suppose we have

type family (a :: Nat) <? (b :: Nat) :: Bool

that computes whether a is less than b, where a type checker plugin does the proof work. For some a, b, and c, if we assume (a <? b) ~ True and (b <? c) ~ True, the plugin can prove (a <? c) ~ True. However, GHC currently provides no way for the plugin to indicate that the proof of (a <? c) ~ True depends on the assumptions. This means that the plugin-produced proof evidence could potentially float out of its desired context, inviting disaster.

In term of Coercions, I propose that the PluginProv constructor of UnivCoProvenance be allowed to include a TyCoVarSet of "free variables" (that is, assumptions) in the proof. Computing the free variables of the enclosing UnivCo would returns these variables, too. It is, of course, up to the plugin to provide the right information here, but plugins generally have enough information to do this correctly (or, at least, to conservatively list all free variables of assumptions as free variables of the conclusion).

Trac metadata

Trac field	Value
Version	8.4.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	dotwani@haverford.edu
Operating system
Architecture

changed milestone to %8.6.1

changed weight to 5

added Tbug Trac import labels

In this case, in principle, shouldn't the evidence produced for the plugin directly depend on the evidence for the assumptions? That is, rather than "proving" (a <? c) ~ True by UnivCo, you would "prove"

  (((a <? b) ~ True, (b <? c) ~ True) => a <? c)
~ (((a <? b) ~ True, (b <? c) ~ True) => True)

by UnivCo and then instantiate it with your evidence for (a <? b) ~ True and (b <? c) ~ True.

That said, your suggestion might make things easier in practice...

added plugins label

But ticket:15248#comment:154469 seems to require a constrained type in the ~ relation, which is generally not allowed. I suppose nothing stops a plugin from producing such things (and GHC might even consume them correctly), but I don't think that's explicitly a supported feature. (You can't say that in source Haskell, for example. Even with quantified constraints.)

Yes: see #15248 on #8095, and the discussion on D4766. PlugInProv should have a TyCoVarSet just as the (upcoming) ZappedProv does, and for the same reasons.

changed milestone to %8.8.1

These won't be addressed in GHC 8.6.

changed milestone to %8.10.1

Bumping milestones of low-priority tickets.

added typechecker plugins label

added Pnormal label

removed milestone

Looks like !611 (closed) trail-blazes the way for this. Exciting! I anticipate that PluginProv won't have to work as hard to maintain its own DVarSet as does ZappendProv, since there's no combining of PluginProvs. Does that sound right to you, @bgamari?