The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

One solution is to do Program Definition so that foo (it :: nil) is typechecked using bidirectional typechecking for inductive values, 

so that "it" is typechecked with the constraint "nat".

-- Matthieu

On Wed, Jun 1, 2016 at 3:37 PM Amin Timany <amintimany AT gmail.com> wrote:

Hi,

It seems that the problem here is that Coq is trying to determine the implicit argument (the type of the list) of cons by type checking “it”. So, you can try casting the type of “it” to the desired type as Jonathan suggests or fix the implicit argument of cons.

Definition bar : nat := foo ((it : nat) :: nil).

Definition bar : nat := foo (@cons nat it nil).

I’m not sure whether this is the kind of solution you are looking for or not.

— Amin

On 01 Jun 2016, at 15:24, Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 06/01/2016 01:22 AM, Gregory Malecha wrote:

Hello --

I'm wondering if anyone has a trick to get tactics-in-terms to fire later?
Here's a somewhat contrived example:

Definition foo (ls : list nat) : nat := 0.

Ltac try_something :=
  lazymatch goal with
  | |- nat => exact 0
  | |- bool => exact true
  end.

Notation "'it'" := ltac:(try_something) (at level 0).

Definition bar : nat := foo (it :: nil).

In the last line, we know that the type of 'it' should be [nat] since [foo]
takes an argument of type [list nat]. However, when the Ltac actually
fires, the goal is a unification variable and therefore neither of branches
of the [lazymatch] matches.

Any hackish tricks to get this to work? Possibly something involving
'Program' or canonical structures?

About tactic-in-term: one can force it to see an instantiated conclusion only by (that I know of) a cast.  In other words, if you can do "ltac:(tac):T", then tac will see T instead of an evar as the conclusion.  However, I don't see how to use that fact to help you here.

-- Jonathan