The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Note that this still relies on typing the produced term by the kernel typechecker at some point,

so one fully-determined proof term has to be chosen.

One great thing about type theory is that you can produce terms any way you want :)

Usually one wants some control on what is produced, and the current type inference 

provides some, with the (informal) guarantee that print(infer(t)) = t. This determinism

can go away as soon as proof search is involved though, through type classes for 

example, and means to ensure that this search is predictable are useful too.

On Tue, Mar 15, 2016 at 10:08 PM Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 03/15/2016 04:25 PM, Matthieu Sozeau wrote:
> Indeed, it seems this would require pretyping (refinement from untyped terms to
> typed terms) to be done similarly to what the old refine tactic did (or Idris
> does AFAIU). You'd have a tactic pretype that takes a untyped term and produces
> a typed one, with clauses like:
>
>     pretype (forall x : T, b) = mkProd x; [pretype T| pretype b]
>     pretype (fun x : t => b) = mkLam x; [pretype t|pretype b]
>     pretype (f a) = refine (_ _); [pretype f|pretype a]
>     pretype ($(tac)$) = tac
>     pretype (_) = try typeclasses eauto
>     pretype (match x with brs) = evar(T : Type); subst T; unshelve (evar (t : ?T));
>          [pretype x| mkCase t; pretype brs]
> I think that would not be too hard to implement (the devil's in the details though).
> I'm not so sure it is desirable to have the regular type inference be
> implemented like
> that, but that would make a fun experiment.
> -- Matthieu

I think I get the idea - and it seems very interesting!  I didn't know
it would even be conceivable to factor typing in Coq out into the
untrusted world of tactics without creating havoc.

So, this would address both of Arnaud's points below.

I find it ironic that, just as people are coming up with interesting
typed alternatives to Ltac, that perhaps these alternatives would need
to rely on Ltac to do typing.

-- Jonathan

>
>
> On Tue, Mar 15, 2016 at 8:36 PM Arnaud Spiwack <aspiwack AT lix.polytechnique.fr
> <mailto:aspiwack AT lix.polytechnique.fr>> wrote:
>
>          Without understanding what the pretyper does, is the implication of not
>          having any backtracking in the pretyper that Coq can't change the
>          decision about the type of any term once it is typed?
>
>      This is correct, but I’d say this should be seen as two things:
>
>       1. There is no backtracking in the pretyper, so it doesn’t know how to
>          produce a second type if a first one has been invalidated
>       2. Even if there was, if it wasn’t implemented using the abstraction
>          provided by the tactics a type couldn’t be invalidated due to a tactic
>          failing
>
>          Does this restriction on backtracking in the pretyper also imply that
>          experimental typed alternatives to LTac, such as MTac, would all be
>          incapable of backtracking after a successful solution of a type?  If so,
>          would the potential solution of the issue for tactic-in-term also
>          improve the situation for MTac-like alternatives?
>
>      I’m not sure about that. It may be. There are certainly benefits to be
>      derived for MTac and the like, but they may be able to get most of the way
>      without solving point 2 above which is the thorny bit.
>
>      ​
>