... | ... | @@ -187,10 +187,9 @@ You can see that |
|
|
This is a natural way to "fill out" GHC's current design, but it does not introduce anything fundamentally new; for example the intermediate language does not change.
|
|
|
|
|
|
* In contrast, the two `foreach` quantifiers are fundamentally new. They allow us to have an argument (visible or invisible) that:
|
|
|
* Can appear in the rest of the type. E.g. `f :: foreach (a::Bool) -> T a -> Int`.
|
|
|
* Is reasoned about at compile time. E.g. `f True x` is type-incorrect if `x :: T False`.
|
|
|
* Is passed at runtime (just like `(Eq a => blah)`).
|
|
|
|
|
|
* Can appear in the rest of the type. E.g. `f :: foreach (a::Bool) -> T a -> Int`.
|
|
|
* Is reasoned about at compile time. E.g. `f True x` is type-incorrect if `x :: T False`.
|
|
|
* Is passed at runtime (just like `(Eq a => blah)`).
|
|
|
|
|
|
|
|
|
* The `foreach ->` quantifier allows us to eliminate the vast mess of singleton types,
|
... | ... | |