Rule out substitutions from type checking/inference

[Ailrun]

Related code snippet: https://github.com/Beluga-lang/McLTT/blob/89e791077a72a9a91083cfa312871ddce06ffdb1/theories/Extraction/TypeCheck.v#L147-L185 or more specifically, https://github.com/Beluga-lang/McLTT/blob/89e791077a72a9a91083cfa312871ddce06ffdb1/theories/Extraction/TypeCheck.v#L180-L185

The problem here is in ci_extend case. We cannot infer the domain context of σ ,, M, but substitutions, in general, cannot have any "checking" mode (as there's nothing able to provide such domain context for checking).

We may need a judgment corresponding to the elaboration to rule out terms not directly written by users.

C.C. @HuStmpHrrr

[HuStmpHrrr]

We never have to check or inference a substitution. Substitutions never appear in a real program. They only occur in the intermediate process. In fact, I think they don't even occur during type checking, given conversion checking is done by NbE.

We should have a declarative judgment for type checking before going into the implementation. Otherwise, it's going to be difficult to prove completeness.

[Ailrun]

@HuStmpHrrr To rule out the case we need some judgement about elaboration as I said, or at least some type_checking_domain-likie. Otherwise I don't see how that can be done, especially for completeness.

[Ailrun]

and I don't think we need a separate typing judgement here for completeness; the algorithm will generate { {{ G |- M : A }} } + { ~ {{ G |- M : A }} }, which itself already is sound & complete.

[HuStmpHrrr]

Let's discuss some time. I don't get it then.

[Ailrun]

Sure. Oh, and as an extension note, once we have cocon, substitutions will appear in a real program, so we need to check a substitution later (but then we have a type that indeed provides the domain, so I hope that then it works without a problem)