Template poly redesign using sort poly #90
Conversation
| ~~~ | ||
| When checking `prod A A` we must ensure that `q` is above Prop, | ||
| and if we had `prod A B` with A and B at different quality variables | ||
| we would have to unify them (in elaboration) or error (in kernel). |
There was a problem hiding this comment.
I guess prod A B with A and B at different qualities would land in Type thanks to above Prop
There was a problem hiding this comment.
but elaboration still need to have some unification otherwise Inductive foo A B := wrap (_ : prod A B) will produce foo : _ -> _ -> Type@{Type|_} I think
| This gives the implicit instance. | ||
| We then check any constraints on the variables and do regular typechecking. | ||
|
|
||
| ## Subject reduction |
There was a problem hiding this comment.
TODO check that no problem appears with constructors
There was a problem hiding this comment.
A priori the same must be done for (partial applications of) constructors otherwise typechecking their parameter arguments will naturally add constraints on the default instance.
| - the indices types and constructor types do not mention the bound univs and qvar. | ||
|
|
||
| NB: the qvar (if there is one) must be "above prop" so should not appear in relevance marks | ||
| (it's always `Relevant`) so eg |
There was a problem hiding this comment.
not fully clear if we want to keep the above_prop restriction
it makes this relevance issue easier but at the cost of needing the kernel to understand above_prop
There was a problem hiding this comment.
In fact we may not need to understand above_prop, we can allow template qualities to be instantiated by anything.
However taking the max of the argument qualities to get the implicit instance may then fail.
This means for instance we can have sigma@{q|a b} : forall (A:Type@{q|a}) (B:A -> Type@{q|b}), Type@{q|max(a,b)} such that
sigma True (fun _ => nat) : Set
sigma True (fun _ => True) : Prop
sigma sTrue (fun _ => sTrue) : SProp
sigma A B : Type@{q|...} if A and B are in the same qvar q
and sigma True (fun _ => sTrue) and sigma A B with A and B at different qvars are errors (elaboration tries to unify the qualities, kernel just errors).
|
|
||
| - it is non mutual (nested is ok) (this rule is in master but maybe we will remove it) | ||
| - its univ declaration has only univ variables unbounded from below | ||
| - its univ declaration has at most 1 qvar variable. |
There was a problem hiding this comment.
perhaps it would make sense to relax this condition, the extra qvars would appear in the parameters but not in the return sort. if we drop the above_prop condition it may be mildly useful, eg could define a template poly
Class foo A B := {}.which can accept both SProp and Type for A and B
| Inductive prod@{q|u v|} (A:Type@{q|u}) (B:Type@{q|v}) : Type@{q|max(u,v)} := | ||
| pair : A -> B -> prod A B. | ||
| ~~~ | ||
| is accepted and the arrow `A -> ...` has relevance mark `Relevant` not `RelevanceVar q`. |
There was a problem hiding this comment.
Why do we want it to be Relevant rather than RelevanceVar?
There was a problem hiding this comment.
so that instantiation is trivial, but this is probably not actually important
| where the `args` types do not mention the bound univs and qvar, | ||
| `q` is either Type or the unique bound qvar, | ||
| and `u` is either constant or one of the bound univ levels. | ||
| - the indices types and constructor types do not mention the bound univs and qvar. |
There was a problem hiding this comment.
We should probably mention the restriction to zero increments over bound template levels in the return sort, as observed in coq/coq#19230. This can be removed if we manage to get the algebraic universes branch in, but for the time being it is a necessary restriction.
| Consider `(fun X:Type@{u} => I X) (P:Type@{v})` | ||
| with `I@{i | csts(i)} (p:Type@{i}) (q:Type@{i}) : Type@{f(i)}` | ||
| and default instance `{i0}` (which must verify `|= csts(i0)`). | ||
|
|
||
| It has type `forall Type@{max(u,i0)}, Type@{f(u,i0)}` assuming | ||
| - `|= csts(u, j0)` | ||
| - `|= v <= u` | ||
|
|
||
| The reduced value `I P` has type `forall Type@{max(v,i0)}, Type@{f(v,i0)}` | ||
| which is NOT comparable to `forall Type@{max(u,i0)}, Type@{f(u,i0)}`!! |
There was a problem hiding this comment.
This problem arises from non linearity of the template universes in the parameters.
Current plan:
- for qualities, we need nonlinearity as we can't put
max(q1,q2)in the return type. So we fix the problem by saying that a partially applied template requires the quality to be Type. - for levels we forbid nonlinearity (the alternative would be to say that we use the implicit instance for partially applied templates, and only get universes from arguments when fully applied; not fully clear which choice is better or if we should do both)
rendered https://github.com/coq/ceps/blob/template-poly/text/XXX-template-poly.md