Make [ELCtx_Alive] a coercion

I made ELCtx_Alive a coercion.

This has several consequences:

• lft has to be a definition instead of a notation. In order to make sure that it will not be unfolded, I made it part of the signature of the lifetime logic
• The parameters of the fn type have to be uncurried, so that the type inference of Coq determines the value of A befor type-checking the external lifetime environment.

What do you think? Is it worth merging as-is or should we use a notation after all?

added 11 commits

• a4ccdbfa...8d79fb29 - 8 commits from branch master
• 1d83e0eb - Make [lft] an Opaque type, when seen from outside of the lifetime logic model.
• 6ce300c7 - Make [ELCtx_Alive] a coercion.
• ad73f4f3 - Make the notation for function types work even if used with more than on variable.

Compare with previous version

I also added a commit to improve the notation for functions, but this is more or less independent from the rest.

lft has to be a definition instead of a notation. In order to make sure that it will not be unfolded, I made it part of the signature of the lifetime logic

I think that's a good idea anyway. I have to say I find glb a horrible name though. My first associations are "glob" (as in, shell globbing) and "global". What about lft_isect or lft_intersect? I am slightly worried about using up ⊓ here, but then if we didn't use it so far I guess this is a great way to use it. Other than that, this commit should go in.

The parameters of the fn type have to be uncurried

This, too, I thought about doing when I added the notation for fn but then was too lazy. So, again, I'm in favor of this anyway.

So yes, absolutely, please merge after we solved the remaining little issues. This makes me very happy :)

I think that's a good idea anyway. I have to say I find glb a horrible name though. My first associations are "glob" (as in, shell globbing) and "global". What about lft_isect or lft_intersect? I am slightly worried about using up ⊓ here, but then if we didn't use it so far I guess this is a great way to use it. Other than that, this commit should go in.

Ok, I'll take lft_intersect then.

This, too, I thought about doing when I added the notation for fn but then was too lazy. So, again, I'm in favor of this anyway.

Ok. I'm a bit surprised that you prefer the uncurried version that feels a bit unnatural to me. A disadvantage is that rewriting may (or may not) become harder, by making Proper instances difficult to infer. Up to now, nothing bad happened.

I have to say I found it fairly unnatural to have three quantifications. If the quantifier was independent of fn, surely there'd be exactly one binder for the quantified-over variable, not three.

added 3 commits

• bb9d135f - 1 commit from branch master
• a30d1b32 - Try making [lrust_typing] non-discriminated to see whether anything changes.
• 99bd5403 - Merge branch 'jh/undiscriminated_hintdb' into jh/alive_coercions

Compare with previous version

added 9 commits

• ad73f4f3...573fcb77 - 5 commits from branch master
• 094097c8 - Make [lft] an Opaque type, when seen from outside of the lifetime logic model.
• 73fe10ef - Make [ELCtx_Alive] a coercion.
• 9ddb6194 - Make the notation for function types work even if used with more than on variable.
• 53d600fc - Notation FP' as a wrapper for FP, so that the arguments are in the right order.

Compare with previous version

mentioned in commit c278f883

merged