Opened 6 months ago

Last modified 6 months ago

#15248 new bug

Coercions from plugins cannot be stopped from floating out

Reported by: goldfire Owned by:
Priority: normal Milestone: 8.8.1
Component: Compiler Version: 8.4.3
Keywords: TypeCheckerPlugins Cc: dotwani@…, adamgundry
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

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

Change History (5)

comment:1 Changed 6 months ago by adamgundry

Cc: adamgundry added

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

comment:2 Changed 6 months ago by adamgundry

Keywords: TypeCheckerPlugins added

comment:3 Changed 6 months ago by goldfire

But comment:1 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.)

comment:4 Changed 6 months ago by simonpj

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

comment:5 Changed 6 months ago by bgamari

Milestone: 8.6.18.8.1

These won't be addressed in GHC 8.6.

Note: See TracTickets for help on using tickets.