The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

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

On Tue, Mar 15, 2016 at 8:36 PM Arnaud Spiwack <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.

​