Make injectivity on closed type families more aggressive

!8820 (closed) has run aground because type inference is not quite clever enough to accept all the code one might want to write with the definitions proposed in Proposal 475, which it implements. This ticket proposes an enhancement to our treatment of injectivity in closed type families so that !8820 (closed) can proceed.

The key bit is this:

type Tuple2 :: Type -> Type -> Type
data Tuple2 a b = MkTuple2 a b     -- a very ordinary pair type

type TupleArgKind :: Nat -> Type
type family TupleArgKind n = r | r -> n where
  TupleArgKind 2 = Tuple2 Type Type

#23135 has more background (which you don't need to reread if you take my motivation on faith), but the interesting scenario produces this Wanted:

[W] TupleArgKind n0 ~ Tuple2 k0 k1

where n0 :: Nat, k0 :: Type, and k1 :: Type are all otherwise-unconstrained unification variables. We would very much like to eventually decide n0 ~ 2, k0 ~ Type, and k1 ~ Type. This ticket here is about how to get from that Wanted to those unifications.

The injectivity annotation on TupleArgKind does not help us here: the RHS of the equation does not match the RHS of the Wanted, because Tuple2 Type Type does not match Tuple2 k0 k1; perhaps k0 and k1 are not in fact Type, and so we don't want to make any incorrect assumptions.

But, actually, thinking harder, it must be that k0 and k1 are Type: there's no other way for TupleArgKind n0 to reduce to something starting with Tuple2. Note, crucially, that TupleArgKind is closed. We see all of its equations. It has only one equation that results in a Tuple2. So that must be the equation that fires. The injectivity annotation then tells us that n0 is 2, we reduce, and then we win.

This can be easily implemented: when searching through a type family's equations for matching RHSs to use for injectivity, we normally use a one-way match to check whether the target (e.g. Tuple2 k0 k1) matches an instantiation of the RHS (e.g. Tuple2 Type Type). But instead of using one-way matching, we could do two-way unification. (The sets of free variables in the target and in the RHS are always distinct; this is ensured upon creation of the type family.) And then if we discover that only one RHS unifies with the target, we've gotten our match and then can use the injectivity info to produce a new equality.

This relies fundamentally on two assumptions: (1) that the type family is closed, and (2) that we want the type family to actually reduce. Point (1) is easily checked. Point (2) is more controversial: maybe the programmer wants to talk about TupleArgKind 3, even though that type is stuck. (I'm using the definition of TupleArgKind written above, with only one equation, not the more complete one in !8820 (closed).) In proposing this change in this ticket, I'm stating that we want to prioritize cleverer inference over support for stuck type families. I think this is the right decision, but perhaps others will disagree.

We could actually go further and do this analysis even without any injectivity annotation. Suppose F a is a closed type family with equation F ty3 = rhs, and we have [W] F ty1 ~ ty2. If rhs unifies with ty2 (and every other equation F ty3' = rhs' of F is such that either ty3' does not unify with ty1 or rhs' does not unify with ty2), then F ty3 = rhs must be the equation to use, and we can safely produce [W] ty2 ~ rhs. No injectivity required! Or maybe we want this extra behavior to be opt-in; we could do so with e.g. type family F a = r | -> r where F ty3 = rhs. Note the -> r "injectivity" annotation saying that the result can be inferred absent other information. (We actually allow ordinary fundeps like this, too, with no variables to the left of the ->. Sadly such a fundep has a different semantics than what I'm proposing here, because fundeps always work in an open-world assumption. But I like the notation.)

The plan

Relevance

We say that an closed-type-family equation F lhs = rhs is relevant for a Wanted [W] F wlhs ~ wrhs iff

• (lhs,rhs) pre-unifies with (wlhs,wrhs) yielding substitution S
• There is no earlier equation that matches S(lhs). See Yikes2 below.

Key point: equations that are not relevant do not need to be considered for fundeps at all.

Notes

• Pre-unification treats type-family applications as binding to anything, rather like type variables. If two types don't even pre-unify, we say that they are apart.

• Why "pre-unifies with" rather than "unifies with"? See "Unifies vs apart from" below.

• lhs and wlhs are of course each a list of types. We don't really form a tuple (lhs,rhs); we just pre-unify the list (rhs_ty : lhs_tys).

Exploiting closed type families: The Algorithm

Suppose

• F a is a closed type family.
• We are trying to solve [W] F wlhs ~ wrhs.
• wrhs is not a type variable or type-family application. See Yikes3 below.
• There are no relevant Givens [G] F lhs ~ rhs. See Yikes4 below.

Then

• IF F has exactly one equation, F lhs = rhs that is relevant for that Wanted

• THEN emit and solve the fundep equalities

  • [W] wlhs1 ~ lhs1
  • ...
  • [W] wlhsn ~ lhsn
  • [W] wrhs ~ rhs See "Yikes1" below.

  with fresh unification vars in lhs and rhs for the quantified variables of the equation

Relationship to explicitly-declared injectivity

Claim. When considering the interaction between the top-level defn of a closed type family F and a Wanted [W] F lhs ~ rhs, this algorithm subsumes the use of explicit injectivity annotations for F. ToDo: prove this.

But note that explicitly-declared injectivity annotations are still useful for closed type families:

• They are used for the "local" interactions between [W] F lhs1 ~ rhs1 and an inert [G/W] F lhs2 ~ rhs2.
• And for self-injectivity [W] F lhs1 ~ F lhs2
• They improve pre-unification. When unifying F t1 and F t2, if F is injective we can unify t1 and t2.

Unifies vs apart from

In the definition of relevance why do we say "wrhs pre-unifies with rhs" rather than (as in the discussion above) "wrhs unifies with rhs"? Answer: see Section 5.2 in "Injective Type Families for Haskell". A concrete example is test T12522a:

newtype I a = I a

type family Curry (as :: [Type]) b = f | f -> as b where
    Curry '[]    b = I b
    Curry (a:as) b = a -> Curry as b

[W] Curry alpha beta ~ (gamma -> String -> I String)

Clearly the RHS is apart from the first equation and we want to fire injectivity on the second equation.

Yikes1: Fundeps from RHS as well as LHS

Consider this from T6018:

type family Bak a = r | r -> a where
     Bak Int  = Char
     Bak Char = Int
     Bak a    = a

and [W] Bak alpha ~ (). Only the last equation is relevant, but we clearly don't want to just produce a new fundep Wanted for the LHS: beta ~ alpha, where beta is freshly instantiated from a. We must also produce an equality [W] beta ~ () from the RHS.

Hence the [W] wrhs ~ rhs in The Algorithm.

Yikes2: Equation shadowing

Consider the same family

type family Bak a = r | r -> a where
     Bak Int  = Char   -- B1
     Bak Char = Int    -- B2
     Bak a    = a      -- B3

and [W] Bak alpha ~ Char. This is more delicate. In fact Bak is injective. You might think that (B3) could be instantiated to Bak Char ~ Char; but actually that instantiation will never fire becuase (B2) Bak Char ~ Int would fire first. So the only way to return a Char is if the argment is Int; so we can emit [W] alpha ~ Int. Hence (B3) is not relevant; only (B2) is relevant.

That is the reason for "There is no earlier equation that matches S(lhs)" in the definition of Relevance above.

A watertight proof that this is the Right Thing is not very easy. See this comment

Yikes3: Termination

We know that generating fresh unification variables during fundeps can lead to non-termination. Here is a tricky case (test T16512a):

  type family LV as b where
     LV (a : as) b = a -> LV as b

  [W] LV as bsk ~ LV as (ask->bsk)

Here as is a unification variable, while ask and bsk are skolems. There is one relevant equation, because there is only one equation in the family! Hence we generate new equalities

              ax:asx ~ as
                  bx ~ bsk
   (ax -> LV asx bx) ~ LV as (ask->bsk)

where ax, asx and bx are fresh unification variables. We can solve:

  as := ax:asx
  bx := bsk

Leaving us with

   (ax -> LV asx bsk)  ~   LV (ax:asx) (ask->bsk)

-->{reduce RHS with the equation for LV}
   (ax -> LV asx bsk)  ~   (ax -> LV asx (ask->bsk))

-->{decompose ->)
   LV asx bsk ~ LV asx (ask->bsk)

And now we are back to where we started! This goes on forever, making a deeper and deeper list. LOOP.

Idea 1: insist that wrhs headed by a generative TyCon. If that isn't the case, the RHS has no information at all to drive improvement.

That seems like the right thing, but I don't see how to prove that it guarantees termination.

Richard offered this example, which would not be caught by the above test.

type family F a

type family C a where
  C [a] = F (Maybe a)

with wanted [W] C beta ~ F alpha. There is only one equation, and it is relevant, so we can try to solve (instantiating a with gamma)

[W] beta ~ [gamma]
[W] F (Maybe gamma) ~ F alpha

We can unify beta := [gamma], and fail to solve the second one. But perhpas that unification will unlock something else which will unify alpha.

Idea 2. An alternative would be to have some kind of "depth" or "fuel" limit. That would work but

• On the way to the limit we'd still be doing lots of unifications. (Say depth 100.)
• So we'll iterate the solver loop
• Each iteration of which will do another 100 unifications.

So we'll end up bulding an 100*N length list before baling out. If that's the best we can do, so be it, but Idea 1 cuts it off (well some cases at least) before it even gets started.

Yikes4: Local Givens

Consider indexed-types/should_compile/CEqCanOccursCheck:

type family F a where
  F Bool = Bool
type family G a b where
  G a a = a

foo :: (F a ~ a, F a ~ b) => G a b -> ()

In the ambiguity check for foo we get

  [G] F a ~ a
  [G] F a ~ b
  [W] F alpha ~ alpha
  [W] F alpha ~ beta
  [W] G a b ~ G alpha beta

Now use The Algorithm above on [W] F alpha ~ alpha. There is only one equation for F, and it is relevant, so we gaily emit the fundep equality [W] alpha ~ Bool, and we are immediately dead. We end up with

    • Could not deduce ‘b ~ Bool’
      from the context: (F a ~ a, F a ~ b)

It is true that the only way a caller can satisfy F a ~ a is by instantiating a to Bool; but we don't have evidence for that which we can use to satisfy b ~ Bool. The trouble is that The Algorithm relies on knowing all the equations for F; but in this case we have some Given constraints that locally extend F.

This relates closely to Note [Do local fundeps before top-level instances] and Note [Do fundeps last] (which are saying much the same thing). These Notes are extremely delicate. If a local Given doesn't give rise to a fundep equation we will currently move on to the top-level fundeps; but perhaps after some other constraints are solved the local Given would fire. Indeed this is exactly what happens above!

Solution: Only run The Algorithm if there are no relevant Givens.

This is much more robust than "only run The Algorithm if attempting local fundeps gives rise to equations" because if a Given is irrelevant is is forever irrelevant.

It's a bit like noMatchableGivenDicts and mightEqualLater for dictionaries. Indeed we should probably apply a similar check when doing fundeps on dictionaries.

Historical note: compatibility

In an earlier version of The Plan we thought we could take advantage of compatibility. But we later concluded that we could not.

First a reminder. Two equations F lhs1 = rhs1 and F lhs2 = rhs2 are compatible iff

• If lhs1 and lhs2 unify with substitution S, so that S(lhs1)=S(lhs2), unify(lhs1,lhs2)=S
• then S(rhs1) = S(rhs2).

NB: two equations whose LHSs are apart are vacuously compatible.

When doing type-family reduction on, say F tys, we work top-to-bottom, finding the first equation that matches. But we only fire that equation if tys is apart from the LHS of every preceding incompatible equation

Example

type family F a b where
  F Int Bool = Bool   -- F1
  F Int a    = a      -- F2
  F a   b    = Char   -- F3

• If (F1,F2) fail to match, (F3) matches, that's not enough to choose (F3). E.g. F alpha Int. Later we might find alpha:=Int. We don't fire (F3) because (F2) is incompatible, but F alpha Int is not apart from it.
• But if (F1) fails to match and (F2) matches, we can fire (F2), because (F2) is compatible with (F1). E.g. F Int alpha: we can reduce this to alpha via (F2); and doing so remains valid even if we discover alpha:=Bool.

So when matching top-to-bottom, we need to check that earlier incompatible are LHS-apart from the thing we are reducing.

Returning to fundeps, consider [W] F beta alpha ~ Bool. Reduction is stuck. Apply the above fundep algorithm.

• We try (F1). (CFD1) holds but (CFD3) fails on (E2).
• So we try (F2). (CFD1) holds, but (CFG2) holds only because (F1) is compatible.

Important: consider

type family G a where
  G Int = Bool   -- G1
  G Bool = Char  -- G2
  G Char = Int   -- G3

and [W] G alpha ~ beta. Not that all equations are (vacuously) compatible. So when we come to (G3) it'll have no incompatible predecessors; so we'll say yes, and unify alpha ~ Char. No no no.

Conclusion the "test only against earlier incompatibles" is wrong. Rather, the earlier equations that we can skip during (CFD2) are those whose

• LHSs unify with the current eqn
• and RHS is the same under that unifying substitution.

NO that is wrong too. Consider

type family H a where
  H Int a = Int
  H a Bool = Int

and [W] H alpha beta ~ Int. The two equations are compatible. But we can't improve alpha:=Int or beta:=Bool because we don't know which is needed. So the example F above is even narrower.