The Coq mailing list

[Sylvain Boulmé <Sylvain.Boulme AT imag.fr>]

Le 06/10/2016 à 11:18, Jean-Francois Monin a écrit :
> Would things get naturally simpler using Set rather than Type in that case?
>
> My understanding is that Set is much simpler than Type, so I stick to
> Set for data structures as much as possible (though it is not trendy).
> For instance, nat: Set.
> Having list : Type -> Type is reasonable in order to have lists
> of anything once for all, including lists of proofs, lists of Props, lists
> of types, etc.
>
> For the case of Sylvain, is Type really needed?

Yes, because my recursive evaluation of expressions instantiates type 
"var" as a complex type that contains "MSets.MSetPositive.PositiveSet.t" 
which is defined in Type in the Standard Library.

But, the trick of Guillaume solves perfectly my issue...

S.



> Jean-Francois
>
> On Thu, Oct 06, 2016 at 09:22:17AM +0200, Guillaume Melquiond wrote:
> > On 06/10/2016 09:13, Sylvain Boulmé wrote:
> >
> > > But, when using this tactic inside a Coq module "TestTactic", I get the
> > > following error message:
> > >
> > > Error: Illegal application:
> > > The term "Syntax.Var" of type
> > >  "forall var : Type, var -> Syntax.expr var"
> > > cannot be applied to the terms
> > >  "v" : "Type"
> > >  "r4" : "v"
> > > The 1st term has type "Type@{TestTactic.1}"
> > > which should be coercible to "Type@{Syntax.1}".
> > >
> > >
> > > How to correct my code above ?
> >
> > As far as I know, you are supposed to call Typing.type_of on your newly
> > created term. That will return a new evarmap that should pass to
> > tclEVARS rather than the old one (which does not contain enough universe
> > constraints for checking that your new term is well-typed).
> >
> > Unfortunately, it means type-checking your term twice, which you
> > precisely wanted to avoid since you are calling exact_no_check. Another
> > solution is thus not too call Typing.type_of on your new term, but on a
> > smaller simpler dummy term. If your dummy term (whatever its type)
> > happens to produce the exact same universe constraints as your new term,
> > then you are good to go and you can use the produced evarmap instead.
> >
> > Best regards,
> >
> > Guillaume