What is unsafe about the Ltac2.Constr.Unsafe module?

Using Coq
1

I find it very handy to have the AST of constr around for writing tactics. However, it is a little unnerving that kind is placed under the Unsafe submodule.

In what sense is it unsafe? Will it cause coq to crash or make my proof unsound?

I saw functions such as is_constructor are exported as safe functions. My guess is that as long as I don’t use the AST to construct terms but only traverse/read the AST as an extension of pattern matching, I shouldn’t run into any issues. Is that correct?

2

The subterms it produces are unsafe, for instance from fun x => x you can get an unbound variable by looking at the body of the function.

3

It’s also the case that the terms you construct can break various invariants (that all de Bruijn indices are positive and bound, that all named variables exist in the context, that evars are in a consistent state, etc) that other parts of the code rely on, resulting in various errors, anomalies, and even crashes.

1 Like