The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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