... | ... | @@ -517,7 +517,7 @@ Note: full-spectrum dependently typed languages treat `t1 -> t2` as a mere abbre |
|
|
`foreach (_ :: t1) -> t2`. But until the Glorious Day, DH will treat these two very
|
|
|
differently:
|
|
|
* If `f1 :: t1 -> t2`, then in a call `(f1 arg)`, there are no restrictions on `arg` (except of course that it has type `t1`).
|
|
|
* If `f2 :: forall (_ :: t2) -> t2`, then in a call `(f2 arg)` arg must lie in the Static Subset of terms.
|
|
|
* If `f2 :: foreach (_ :: t2) -> t2`, then in a call `(f2 arg)` arg must lie in the Static Subset of terms.
|
|
|
Even once we reach the Glorious Day, nothing forces us to unify `t1 -> t2` with `foreach (_ :: t1) -> t2`, and
|
|
|
we may decide not to.
|
|
|
|
... | ... | |