Version 6 (modified by goldfire, 5 years ago) (diff)

--

This page is to document various decisions / important emails / conversations that have come up in the course of implementing DependentHaskell. There is no effort at making the material here understandable to those not in the conversations. (Some of these conversations are with myself [= Richard Eisenberg], making the situation even worse.) There is also no concerted effort at a logical organization of this page.

## Roles, Coherence, and Kinds

### Email sent from RAE to SCW on 7/14/14

I've hit an unfortunate conflict between roles and "nokinds" and want some advice on how to merge them. I have a potential answer, but it involves introduce a second, symmetric form of coherence (but with different roles), and that feels wrong.

The problem all starts with casts:

```t : k1
g : k1 ~ k2
---------- CastTy_NoRoles
t |> g : k2
```

Uniformity with the term level suggests the following:

```t : k1
g : k1 ~R k2
------------- CastTy
t |> g : k2
```

Notice that g is representational.

Now, we must consider how coherence should work. Here is an attempt:

```g : t1 ~r t2
t1 |> h : k          -- that is, (t1 |> h) is well-formed
-------- Coherence1
g |> h : (t1 |> h) ~r t2
```

Note that `r` is a role metavariable; it is NOT (necessarily) "representational". The role of (g |> h) is the same as the role of g. Now, suppose we have (axAge : Age ~R Nat). Then, (<Zero> |> axAge) : (Zero |> axAge) ~N Zero. In other words, (Zero |> axAge) and Zero are nominally equal. This is disconcerting, though, because nominal equality should be the equality that the type-checker infers... and yet, casting by axAge is not inferrable; the user must put in a `coerce`. So, rule Coherence1 seems wrong.

```g : t1 ~r t2
t1 |> h : k
------------- Coherence2
g |> h : (t1 |> h) ~R t2
```

The Coherence2 rule allows g to have any role, but it restricts (g |> h) to be representational. Coherence2 would mean that nominal equality is not coherent! This seems troubling, too. (It would also break the lifting lemma, which crucially relies on proper coherence of all three equalities.)

My current adopted rules are these:

```g : t1 ~N t2
t1 |> (sub h) : k
--------------------- Coherence_Nom
g |> h : (t1 |> sub h) ~N t2

g : t1 ~R t2
t1 |> h : k
------------------- Coherence_Rep
g |> h : (t1 |> h) ~R t2
```

These rules require that g and h have the same role, which is also the role of (g |> h). The problem here is that the lifting lemma breaks. Recall that the lifting lemma works with a substitution S from type variables to coercions. (It's slightly more involved, but this is a convenient simplification.) Let SL be the type-variable-to-type substitution that maps the domain of S to the left-hand types of the range of S. Define SR similarly, on the right. Then, then lifting lemma states that S(t) : SL(t) ~ SR(t). In the presence of roles, the lifting operation must also take an input role, making the lemma look like: S(t)_r : SL(t) ~r SR(t). See pages 19-20 of the extended version of the Coercible paper for the details.

We must choose an implementation for S(t |> h)_r. We know, by induction, that S(t)_r : SL(t) ~r SR(t). We need a coercion of type (SL(t) |> SL(h)) ~r (SR(t) |> SR(h)). In the "nokinds" paper, we achieved this by using coherence on S(t) -- no problem. But, with the last two rules I wrote above, this doesn't work! `h` has the wrong role to use in a coherence, if the desired role is nominal, because `h` is representational, as we can see by its use in the cast (t |> h). We're stuck.

The solution I have in mind is represented by this rule:

```g : t1 ~N t2
h : k1 ~N k2
t1 |> h1 : k1
t2 |> h2 : k2
------------ NomCoherence
g |>>_h (h1, h2) : (t1 |> h1) ~N (t2 |> h2)
```

Here, I've defined a new form. This is quite like a symmetric form of Coherence1, but it requires the target kinds to be *nominally* equal, which is a stronger requirement. This form would work in the lifting lemma fine: S(t |> h)_N = S(t)_N |>>_(S(k)_N) (SL(h), SR(h)), where k is the kind of (t |> h). Note that we still need the asymmetric coherence to deal with lifting context extension for existential variables (Def'n 5.6 of p. 9 of the "nokinds" paper).

I don't see any real problems with introducing the new form, except for the extra weight it causes. And, having two very similar, but subtly different coercion forms just smells like there is a better design out there.

### Result of ensuing discussion

Go with Coherence1. No actual problems are caused by it, and we don't have a semantics of nominal equality that we're aiming for, so there's nothing terribly wrong here.

### Conversation on 11/7/14

SCW said that Coherence_Nom + Coherence_Rep + NomCoherence was better. NomCoherence is actually more like the other congruence forms that we have in coercions. The only reason it's missing from the "nokinds" paper is that we can derive it from the other coherence rule. And, if we did have a semantics for nominal equality, Coherence1 would be questionable.

RAE's decision after conversation: Continuing with Coherence1, noting SCW's disagreement. Reasons for this decision:

1. The decision to go with Coherence1 was a result of another (less well-documented) conversation with SCW. Thus, there's not a clear, unchanging stance of the person with more experience.
2. The cost of changing from Coherence1 to the 3 other rules is not likely to change if I continue more work based on Coherence1.
3. There's a good chance that only one of these two possibilities is "Right". We'll know more later.
4. I'm eager to make forward progress and not spin around this wheel again.

## Lifted vs. Unlifted equality

GHC happily keeps a distinction between lifted and unlifted equality, but this is causing me grief. The primary cause of the grief is that I need to cast types by unlifted equality (casting by lifted equality is bogus because the evidence might be bottom), and there is no type-level construct to unpack a lifted equality. Here is the canonical example:

```data SameKind (k :: *) (a :: k) (b :: k)
challenge :: forall (k1 :: *) (k2 :: *) (a :: k1) (b :: k2). (k1 ~ k2) => SameKind k1 a b
challenge = ...
```

During translation to FC, we have to give a name to `k1 ~ k2` (easy) but then somehow use it to cast `b` to have kind `k1`.

### Equality today

This problem provoked me (and SCW) to think about why we need lifted equality at all. Currently (7.8.3), this is the story:

1. The user writes lifted equalities only.
1. Lifted equality is defined like
```data a ~ b :: Constraint where
Eq# :: a ~# b -> a ~ b
```
1. The solver thinks in terms of lifted equalities only.
1. Casts (only in terms, of course!) use unlifted equalities.
1. The desugarer uses the result of the solver (the various `EvTerm`s and `EvBinds`s) to create and use lifted equalities. To use the lifted equalities in casts, the desugarer inserts `case` statements to unbox the lifted equalities. This is in `dsTcCoercion`.
1. GADTs are rejigged in terms of lifted equality for the wrapper, but the worker is in terms of unlifted equality. This is important, because we don't want to make space to store the equalities! The wrapper unboxes before calling the worker.

### Recent developments

In recent Skype calls, I've discussed the issue with SPJ and DV, among others. Here are some the points that came out of these conversations:

1. Once upon a time, equality evidence was all unlifted and considered to be a type variable. This caused endless havoc, because all other evidence (dictionaries, implicit parameters) are term variables.
1. A refactoring made equality just like other evidence: lifted and term-level.
1. Looking back, we questioned whether making equality lifted was necessary, while agreeing that it fits much better at the term level.
1. The solver could just as easily work over unlifted equality. It would be a simplification, actually, in that the desugarer would no longer have to box and unbox. (The unnecessary boxing/unboxing is later removed by the simplifier.)
1. A potential snafu is that the solver can spit out mutually-recursive groups of bindings. We, of course, cannot put an unlifted binding in a recursive group. So, the plan is to push the unlifted bindings into the RHSs of the letrec group, and use non-recursive lets. For example:
```let x :: C a = ... z ...
y :: t ~ s = ... x ...   -- class C could have an equality superclass
z :: t ~# s = unbox y
```

becomes

```let x :: C a = let z :: t ~# s = unbox y in ... z ...
y :: t ~ s = ... x ...
```

Simon has spotted a tricky bit here, but I can't recall it. Simon?

1. Another small annoyance with unlifted equality is deferred type errors. This can likely be mitigated by floating in the (now-strict) calls to `error`.
1. The bigger problem with unlifted equality is that unlifted things -- for good reasons -- can't be abstracted over. For example, if we have
```data Dict c where
Dict :: c => Dict c
```

it would be disastrous if `c` could become `a ~# b`. So, users still need to work in terms of lifted equality.

1. I proposed a plan of redefining lifted equality thusly:
```class a ~# b => a ~ b
instance a ~# b => a ~ b
```

Let's call this redefined lifted equality `~2`. Although the internal representation of `~2` is the same as that of `~`, the treatment in the solver would differ significantly. When the solver sees `~2`, it would just access the superclass (in the case of a given) or the one instance (in the case of a wanted), and then the real equality solving would happen over `~#`. This has the advantage of simplifying the desugarer, but still requiring the let-pushing in point 5, above. But, this is a big win for me because I need the solver to work over unlifted equality for kind casts, so using `~2` instead of `~` would mean that the solver works over only 1 equality type. There were no objections to this plan, as of Nov. 8, 2014.

The point articulated directly above seems to be a nice resting place for this discussion, and it is my plan of record going forward. However, because my current hybrid solver (that works over both `~` and `~#`) is chugging along, doing this redesign is not a high priority. Furthermore, this plan does not fix my original problem, of needing unlifted equality in types.

### A simple solution to the `SameKind` problem

When users write `~`, it means lifted equality, unless unlifted equality is necessary. In the latter case, `~` means unlifted equality.

For easy reference, here is the challenge:

```data SameKind (k :: *) (a :: k) (b :: k)
challenge :: forall (k1 :: *) (k2 :: *) (a :: k1) (b :: k2). (k1 ~ k2) => SameKind k1 a b
```

When type-checking and desugaring the type of `challenge`, above, we can discover that the `k1 ~ k2` equality must be used "right away". Under my proposal, this means that the `~` would simply be interpreted as unlifted. This is possible at all because we can discover -- crucially, in the same type -- the need for unlifted equality quite easily. Thus, `challenge`'s type is translated to FC like this:

```challenge :: forall (k1 :: *) (k2 :: *) (a :: k1) (b :: k2) (c :: k1 ~# k2). SameKind k1 a (b |> sym c)
```

How can this be implemented? That's a little more challenging because type-checking and desugaring happen in the same pass (unlike for terms). By the time we've discovered that we need unlifted equality, the equality constraint has already been desugared from `HsType` to `Type`. There's a great trick we can pull here, though: parameterize `~` by a levity variable! (See NoSubKinds.) This unifies the types `~` and `~#`.

We create a new type

```EQ# ::  forall (v :: Levity) (k1 :: *) (k2 :: *) (a :: k1) (b :: k2). TYPE v
```

That is, `EQ# Lifted` is good ol' `~` and `EQ# Unlifted` is just `~#`. When a user writes `~`, it desugars to `EQ# alpha`, where `alpha` is a levity metavariable. If this variable is still unconstrained when we're done type-checking the type, it defaults to `Lifted`. If an equality is used within the type, the type-checker will set `alpha` to `Unlifted`. This is very similar to the treatment of levity metavariables that arise when type-checking `->` or `error`. This idea also has the nice advantage of getting rid of `~` and `~#` as separate tycons within GHC -- we can now just talk in terms of `EQ#`.

Simon has pointed out that users may still eventually want control over this inference. So, here is the concrete plan: lifted equality is denoted by `Equal` in user code; unlifted equality is denoted by `Equal#`. The notation `~` means, essentially, `EQ#` -- that is, infer whether to use `Equal` or `Equal#`. This should be fully backward-compatible.

This is all really quite pleasing to me, as it seems to simplify things somewhat, rather than complicate them. That's a great thing when it happens.

Question: What is the kind of `Equal#`? I propose `forall k1 k2. k1 -> k2 -> Constraint#`.

### Some non-solutions to the `SameKind` problem

It seems worthwhile to jot down some failed ideas of how to solve `SameKind`:

1. Write a type family `Cast`:
```type family Cast (k1 :: *) (k2 :: *) (a :: k1) (g :: k1 ~ k2) :: k2 where
Cast k1 k2 a (Eq# g#) = a |> g#
```

This type family does the unboxing and then casts. If the supplied lifted equality evidence is not `Eq#`, then the type family application is stuck, as it should be.

This doesn't work because it's not compositional. If we have an equality for `Maybe a ~ Maybe b`, we can't case from `a` to `b`. This is because we can't use the coercion formers anywhere. A solution here is to just write type families that lift each coercion former into lifted equality. This works in every case but the `forall` coercion former, which can't be written as a type family because it binds a variable locally. If we had type-level lambdas, this approach could work.

1. Have `~` always mean unlifted equality.

This doesn't work because we then can't abstract over equality predicates.

1. Write a type family `Unbox`:
```type family Unbox (k1 :: *) (k2 :: *) (g :: k1 ~ k2) :: k1 ~# k2 where
Unbox k1 k2 (Eq# g#) = g#
```

The problem here is that we certainly can't call a type family from within the coercion grammar. There's no way of using `Unbox`! Even if we made space somehow for just this one type family, when would it get "evaluated"? Never, so the system is broken.

1. Introduce `case` into types.

This actually works (I think) and shouldn't cause any undue wrinkles. The `case` would simplify through iota-reduction axioms that get applied (still no computation within types), but I think this could work. But, it's decidedly not simple.

## Open questions

1. What is the kind of `Equal#`? I propose `forall k1 k2. k1 -> k2 -> Constraint#` for a new kind `Constraint#`.
1. What are the restrictions on the use of `Constraint#`s in tuples, superclasses, and such?
1. What checks should Core Lint do about levity polymorphism? Where is it allowed and where is it not allowed?

# `TcTyVars`

This is from emails with SPJ & DV on 12/31/14:

RAE: 1) Is there a reason to have `SkolemTv False` TcTyVars separate from proper, zonked TyVars? There is some effort at switching back and forth between proper TyVars and skolems, but I'm not sure why. I even recall finding a case (we talked about it -- I forget the Trac #) where a skolem tyvar got past zonking and into Core, with no ill effect. Conversely, TyVars are seen during kind unification (see comments toward end of TcUnify), also to no ill effect.

SPJ: Well my original invariant was supposed to be:

the typechecker sees only TcTyVars (except perhaps as the quantifier of a forall)

the rest of the compiler never sees a TcTyVar

The SkolemTv False thing was just to ensure this. You'll see lots of ASSERTs for isTcTyVar which would fail if we used a TyVar. But I think nothing would actually go wrong if we allowed TyVars. And as you observe, the invariant is not rigorously observed.

Originally SkolemTvs had lots of SkolemInfo in them, but they don't any more.

RAE: In my branch, this change may be somewhat forced, for exactly the same reason that sometimes TyVars appear during kind unification. Of course, with type=kind, then the TyVars can appear anywhere! I won't actively actually remove SkolemTv for now (too much is broken at the moment, and this would only break more things!), but I won't care too much about the distinction, with a note to myself to clean this up later.

RAE: 2) In the TcS monad, there are two facilities that accomplish the same goal but with very different mechanisms: meta-tyvars and EvBindsVar stuff. Both allow in-place updating of types or coercions, but one does it in a distributed manner (meta-tyvars) and one via a central master list of bindings (EvBindsVar). Is there an advantage to having these different mechanisms?

SPJ: The original idea was that the solver would be pure. It would have no side effects, and so in principle you could do backtracking search without having to undo side effects. The TcS monad even carried a TvSubst which we used instead of side-effecting updates of the meta-tyvars. When exiting the TcS monad we applied the substitution in a side-effecting way.

But (a) there was no powerful motivation for the goal of purity. The only place we try search is in TcSimplify.disambigGroup when we see if we can solve things by filling in a meta-tyvar with Int, or Integer, or Float, etc. But that's now done another way.

Moreover (b) the goal of purity was never achieved. Reason: the EvBindsVar stuff. The solver solves an entire tree of constraints, side-effecting bindings in the EvBindVars kept at various points in the tree. These EvBindsVars are also referred to from the HsSyn tree. Now, we could have maintained a substitution from EvBindsVar -> EvBinds, and applied that when exiting the substitution, but I never tried that.

Finally (c) if you don't need to undo things, then side-effecting substitution is very efficient! (At least I think so; I have not actually measured it.) Building a functional substitution and subsequently applying it by side effect seems necessarily slower.

So I removed the functional TvSubst and do both the EvBinds and meta-tyavar by side effect.

RAE: Is there something to be gained by unifying these approaches?

SPJ: Actually they are the same already. In both cases we update a mutable variable. In the EvBinds case it's not a single central "master" list; each Implication has its own EvBindsVar, which becomes the ambient one when we walk inside the Implication.

RAE: But, with this approach, zonking becomes simply applying a substitution, no? Continuing on from my first point, above, it might be possible to eliminate TcTyVars entirely. This would seem to be a nice simplification: no more zonking as a separate algorithm (2, actually!), and no more instSkolTyVars. (Zonking inside the knot would perhaps need to remain, as applying a subst can be strict in TyCons...)

SPJ: You seem to be suggesting extending the functional-substitution idea outside TcS to TcM. Yes, we could do that. But in effect the mutable store *IS* a single, global, ambient substitution! But one that is implemented by the memory system. So what would be gained, really?

RAE: 3) Part of recent refactoring allows the TcS monad to update a meta- tyvar directly, with setWantedTyBind. In some places, the code that calls setWantedTyBind then kicks out relevant bits of the inert set. In other places, there is no kick-out. I would think we would always want to kick out after setWantedTyBind, but perhaps I'm missing the subtleties of fmvs and such.

SPJ: The kick-out stuff is necessary only when we have an active InertCans and work-list; ie during TcInteract. Outside that, it doesn't matter.

RAE: Specifically, I'm worried about defaultTyVar, which is misbehaving on me. Relatedly, does Note [DefaultTyVar] still apply when there is no sub-kinding?

SPJ: When there is no sub-kinding I think we can get rid of defaultTyVar altogether. But maybe something different happens instead? What happens with the example in the Note?

```    instance Show (a->b)
foo x = show (\_ -> True)
```

What kind do you get for `p` in the `Show (p -> q)` constraint?

RAE: This doesn't really change.

We infer `(\_ -> True) :: (c -> Bool)`, where

``` c :: TYPE v
v :: Levity
```

and `c` and `v` are meta-vars. The instance doesn't apply because the kind of `a` in the instance is *, distinct from the kind of `c`. Defaulting (in my branch) simply writes `v := Lifted` using setWantedTyBind. So we have all the same issues at play, just with a different underlying mechanism.

# Separating `TcType` from `Type`

Also from emails 12/31/14.

SPJ: On this question, I had been thinking about a more radical solution: make TcType and Type into distinct types, just as TcCoercion and Coercion are different.

A powerful reason for doing this is that TcTypes could have location information at every node in the tree, which is good for error reporting; Lennart gave a great talk at the Haskell Implementors Meeting about this. Another reason is that we'd have a static guarantee that there were no meta-tyvars surviving after typechecking.

There are minor things too. For example, we could have a special constructor for type-function applications.

How hard would this be? For much of the code it'd be easy. E.g. a global Id contains a Type, which must be instantiated to a TcType even if it has no quantifiers. A local Id would be a TcId, not an Id, with no IdInfo but with other info currently stored in the ATcId structure.

I'm quite sure there would be some dark and tricky corners, perhaps around the places where our current invariant doesn't quite hold. But sorting them out would make everything cleaner and more robust.

It's a big, unforced change. But I think it would be a jolly good thing.

Any opinions?

RAE: Funny -- I just ran across a different place (in my branch) where this was called for.

My need is that the type-checker thinks in terms of TcCoercions, and occasionally needs to cast a type by a TcCoercion. Of course, Type has no room for such a cast. I've carefully avoided making this a problem, using two tricks:

• I've rejigged TcUnify.uType & friends to produce a Coercion, not a TcCoercion. This was straightforward, now that we can inject a Coercion into a TcCoercion (unifyType, the exported function, still produces a TcCoercion). But, now uType can deal with the heterogeneous case.
• In the solver, the same problem happens, but the solution isn't so easy. Say we have a Type s and a TcCoercion tco. We wish to write (s |> tco), but this is ill-formed. So, I create a new covar c of the same type as tco, bound to tco. I can then use CoVarCo to put c in a Coercion, and make (s |> c). When desugaring, this all works out, because any lifted coercion variables in a TcCoercion get unboxed, so all is good in the end. But, this all smells wrong.

And, it's always possible I'll come across a case where I need a type casted by a TcCoercion and no trick works.

With this change, it also opens up the door to separating desugaring of types from type-checking. The TcType could support wrappers, like HsExprs do. I currently don't think we'll need wrappers in types to implement dependent types, but I could very well be wrong.

While we're at it, we could be more general in the form of annotation. The flattener would awfully like to know whether a type is fully normalised w.r.t. type families, but that would have to be stored at every node.

I'm generally of the opinion that more types are better, unsurprisingly. (I've wanted to separate out Id, CoVar, TyVar, and TcTyVar for some time, along similar lines.)

My guess is that this change would decrease performance in places, with the extra conversions. Would this be significant? Probably not, but worth noting as a "con".