... | ... | @@ -116,3 +116,83 @@ The second point seems to be the right way to allow levity polymorphism. If the |
|
|
|
|
|
|
|
|
The actual implementation should be easy: add parsing support for TYPE and then check for levity-polymorphism in `checkValidType`. The inference algorithm should remain unchanged, as a levity-polymorphic type would never be inferred, just checked. This extension is left as future work.
|
|
|
|
|
|
### Issues from Dimitrios
|
|
|
|
|
|
**Note Apr 15**: These issues are absolutely present in Richard's current implementation.
|
|
|
|
|
|
- We need a Lint check for what types are OK; i.e. which FC programs are well typed.
|
|
|
|
|
|
- Proposed criterion: **`(ty:TYPE l)` cannot occur on the left of an arrow, or in the type of any binder**. And hence not as a field of a constructor, because then the constructor's type is illegal.
|
|
|
|
|
|
- `(Int -> (ty:TYPE l)) -> Int` is ok
|
|
|
- `((ty:TYPE l) -> Int) -> Int` is not ok
|
|
|
- `data T l (a:TYPE l) = MkT (Int -> a)` is ok.
|
|
|
- And so `MkT Unlifted Int# (\n -> error Unlifted Int# "urk")` is ok.
|
|
|
- Moreover the top-level defintion of `undefined` is also ok because `undefined :: forall v. forall (a:TYPE v). a`
|
|
|
|
|
|
|
|
|
You make it sound as if the only problem is defaulting. But I do not think it is enough. For instance, what prevents a user from writing:
|
|
|
|
|
|
```wiki
|
|
|
f :: forall v. forall (a :: TYPE v). a -> a
|
|
|
f x = x
|
|
|
```
|
|
|
|
|
|
|
|
|
The only plausible explanation from that subsection is that TYPE and levities are not exposed to programmers, so they can't shoot themselves in the foot. \*However\* there are cases where you \*must\* expose levities to programmers, for instance to give a signature to an eta-expansion of "error". Example:
|
|
|
|
|
|
```wiki
|
|
|
g :: forall (a:*). forall v. forall (b :: TYPE v). Show a => a -> b
|
|
|
g x = error (show x)
|
|
|
```
|
|
|
|
|
|
|
|
|
So, the statement that "the only complication for GHC is defaulting" is a pretty big understatement. How will you prevent the bad "f" above but allow the good "g"?
|
|
|
|
|
|
|
|
|
Now, I agree with you that defaulting is part of the solution but, what we really would like is to ensure that levities on the left of an arrow cannot be abstracted over. For instance, imagine the following hypothetical typing of (-\>):
|
|
|
|
|
|
```wiki
|
|
|
(->) :: forall v1,v2, FIXED v1 => TYPE v1 -> TYPE v2 -> *
|
|
|
```
|
|
|
|
|
|
|
|
|
Where the `FIXED v1` is like a derived kind class constraint emitted during kind inference (but of course there's no associated evidence with it), which prevents a levity variable from getting generalized. Hence, during type inference:
|
|
|
|
|
|
```wiki
|
|
|
FIXED Lifted => is just discharged successfully
|
|
|
FIXED Unlifted => is just discharged successfully
|
|
|
```
|
|
|
|
|
|
|
|
|
However, in the end of type inference we will be left with constraints of the form:
|
|
|
|
|
|
```wiki
|
|
|
FIXED levity_unification_variable ==> can be defaulted to Lifted
|
|
|
(this will allow us to infer sound types)
|
|
|
|
|
|
FIXED levity_skolem_variable ==> are genuine errors!
|
|
|
```
|
|
|
|
|
|
|
|
|
I don't think it would be that hard to generate kind constraints like the `FIXED` kind class, and treat them specially during defaulting, would it? In fact this might be something we want to introduce to GHC \*today\* even without sucking in the fully glory of your kind equalities, is my guess.
|
|
|
|
|
|
|
|
|
Interesting example
|
|
|
|
|
|
```wiki
|
|
|
g :: (forall a. (# a, a #)) -> (# Int, Int #)
|
|
|
{-# NOINLINE g #-}
|
|
|
g x = x
|
|
|
|
|
|
foo _ = g (# error "a", error "b" #)
|
|
|
```
|
|
|
|
|
|
|
|
|
Some conclusions:
|
|
|
|
|
|
- `forall (l:Levity). ty` has kind `*`. We think of it as a pi, a value abstraction. So `undefined :: forall l. forall (a:Type l). a` has a type whose kind is `*`, and is *lifted.
|
|
|
*
|
|
|
|
|
|
- The body of a type forall should have kind `Type l` for some levity `l`, and that is the kind of the forall. That is, the body cannot have kind `* -> *`, and certainly not `k`. This makes `forall k (a::k). a` ill-kinded. (Cf [\#10114](https://gitlab.haskell.org//ghc/ghc/issues/10114).) |