Feature request: switch from infer to check when given "concrete" infer pattern

[wilbowma]

Not actually sure this is possible, but it ought to be, intuitively.

For context, I'm starring at this line
https://github.com/wilbowma/cur/blob/turnstile-merging/cur-lib/cur/curnel/turnstile-impl/dep-ind-cur2%2Bdata2.rkt#L346

This line annoys me because it branches on the number of parameters and indices, but actually has nothing to do with the number of parameters and indices. Instead, it is giving better inference and error messages by switching to check mode instead of inference mode when possible. This is possible to do this when we would be generating a pattern that is actually a concrete type, and it happens to be the case that we would generate a concrete type when there are 0 parameters and indices.

It seems like Turnstile ought to be able to detect when a infer pattern is actually concrete syntax instead of a pattern, and automatically switch from infer to check in that case. If so, it would be a great feature, as it would automagically improve a user's type system.

This situation probably doesn't come up so much in source Turnstile, but comes up any time we use this pattern variable instantiation technique, i.e., when generating Turnstile.

[stchang]

Pasting the actual lines of code here, since the code is constantly changing

        #,(if (zero? (+ num-params num-idxs))
              ; NB: Again, must handle id transformers differently.
              ; Luckily, we can also be in checking mode in that case.
              #'[⊢ v ≫ v- ⇐ TY]
              #'[⊢ v ≫ v- ⇒ (TY-patexpand A ... i* ...)])

So you would like to only write the second case, and when A and i* are empty, it automatically switches to checking because (TY-patexpand) is not actually matching any new pattern variables?

[wilbowma]

Right.