Imprecise typing error location if discriminee of Ltac2 match!/lazy_match! is not a constr

[samuelgruetter]

cat ltac2_imprecise_error_pos.v

Require Import Ltac2.Ltac2.

Ltac2 foo(b: bool): bool :=
  let c := b in
  match! c with
  | true => true
  | false => false
  end.

coqc ltac2_imprecise_error_pos.v 

File "./ltac2_imprecise_error_pos.v", line 3, characters 0-102:
Error: This expression has type bool but an expression was expected of type
constr

The reported error position spans the whole function, starting at the L of Ltac2, going all the way to the . at the end.

Desired behavior: Only the text between match! and the with should be reported in the error.

coqc -v

The Coq Proof Assistant, version 8.16.0
compiled with OCaml 4.13.0

[JasonGross]

Presumably this is a more general problem of Ltac2 notations and error messages that arise in the inlined notation not having an inverse mapping that says what part of the shorthand is at fault?

[SkySkimmer]

Probably we raise with a loc where the notation is defined, but since we don't allow error locs that aren't inside the current command it gets replaced with the more general loc.

[SkySkimmer]

Probably we raise with a loc where the notation is defined, but since we don't allow error locs that aren't inside the current command it gets replaced with the more general loc.

Actually this is technically true but not useful: we raise with the loc of t in the notation's body

Ltac2 Notation "match!" t(tactic(6)) "with" m(constr_matching) "end" :=
  Pattern.one_match0 t (* <- here *) m.

but that location isn't very user friendly.

The typing process desugars the notation into

fun (b : bool) =>
let c := b in
let m := (* some stuff *) : _ Pattern.constr_matching
with t := c in
Pattern.one_match0 t m

m can get an annotation because the constr_matching scope can't produce any type, but t(tactic(6)) is not so informative.

And even the annotation for m has limits, eg

Ltac2 Eval
  (match! 'true with
  | true => 'true
  | false => 'false
  end : bool).

puts the error location on the whole command.

I think ultimately we want most notations to be typed ahead of time, so match! knows that it's t : constr, m : 'a constr_matching |- 'a.

TBH I'm not sure there's much use for untyped notations, the type system is restricted enough that interesting notations seem to only use their arguments monomorphically (ie can infer their types) and I'm not sure it's possible to use more than prenex polymorphism (because they get desugared to let args := stuff in body) (could be annotated if we wanted).

cc @JasonGross have you used ltac2 notations in a way that seems to require a delayed typechecking?

[JasonGross]

I have not tried to do anything very tricky with Ltac2 notations. If I try to imagine uses for non-monomorphic notations, the thoughts I have are:

1. simulating dependent types (not sure if there's a relevant use) (can we write Ltac2 Notation "foo" x "as" y := x : y and then do foo 5 as int?)
2. making use of mutability in a way that can't be expressed in the type system (can a notation be written that works only when the argument it's passed in some slot is mutable?)
3. expressing row types (a notation that works as long as its argument is a record type with a field named foo)
4. if Ltac2 has open types (does it?), then polymorphism over any open type, where you match the argument against `foo

Ltac2 doesn't really have enough untyped primitive syntax to want untyped notations IMO. The untyped primitive syntax is just type ascription, assignment, field lookup, match?

[SkySkimmer]

Not sure what you call untyped syntax but notations are globalized, so eg Ltac2 Notation "foo" x := x.(bla) refers to the projection bla which is currently in scope, not any projection named bla.

can we write Ltac2 Notation "foo" x "as" y := x : y and then do foo 5 as int

No

[JasonGross]

Can you write Ltac2 Notation "set" x "to" y := (x := y)? If not (or if this sort of thing doesn't work), then it sounds like there might not be any current possible uses for untyped notations.

[SkySkimmer]

I don't think x := y corresponds to any syntax

[JasonGross]

Ah, I guess it's just ltac2_expr0 .( qualid ) := ltac2_expr5, having taken another look at the documentation. In that case, I'm inclined to think that you're right that everything can be annotated with prenex polymorphic types.

[JasonGross]

Hmm, would the situation be different if we had global mutable state a la #13982 (comment) (Ltac2 Notation "myset" x(ident) ":=" y := Set x := y.? Or would let-bindings kill this because we can't ever give y a type?)