The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

On Thu, 3 Dec 2020 14:23:36 +0100
Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

> On 03/12/2020 04:33, jonikelee AT gmail.com wrote:
> > Did anyone know that it works to define Ltac in a Module Type, such
> > that instantiations of that Module Type with an instantiated Ltac
> > def (mostly) works?:
> > 
> > This is in 8.12.  I haven't tried Ltac2 yet - hopefully, the
> > instantiations are required to type match the abstration.  Also, I
> > think it would be better if End Burp produced an error due to the
> > missing tac instantiation, instead of deferring the error (as an
> > Anomaly, no less) until runtime.  That is, assuming this is all
> > intended behavior, which I hope it is...  Is it?  
> 
> It's known, and can be considered a feature-ish bug. It's essentially
> a variant of the trick described here:
> 
> https://github.com/coq/coq/issues/2199

yup.  I should remember that, sometimes, the issue tracker makes an
excellent refman addition.

> 
> Please don't do that in Ltac2 though, this is a known source of type
> unsoundness which is currently not fixable in the current module
> architecture. The best we can do is to forbid the definition of Ltac2
> types inside a module type, but even there one can probably weasel
> their way around using Include.
> 
> PMP
> 

Perhaps there might be some consideration in the future for how
to modularize Ltac2 code in a type safe way?