Opened 4 months ago

Last modified 7 weeks ago

#15589 new bug

Always promoting metavariables during type inference may be wrong

Reported by: goldfire Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler Version: 8.4.3
Keywords: TypeInType Cc: A.SerranoMena@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Currently, when checking a type signature, GHC promotes all the metavariables that arise during checking as soon as it's done checking the signature. This may be incorrect sometimes.

Consider

{-# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,
             AllowAmbiguousTypes #-}

import Data.Proxy
import Data.Type.Equality
import Data.Type.Bool
import Data.Kind

data SameKind :: forall k. k -> k -> Type
type family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where
   IfK (_ :: Proxy True)  f _ = f
   IfK (_ :: Proxy False) _ g = g

y :: forall (cb :: Bool) (c :: Proxy cb). cb :~: True -> ()
y Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d
             x = undefined
         in ()

This panics currently (#15588), but I'm pretty sure it will erroneously be rejected even after the panic is fixed. Let's walk through it.

  • We can derive IfK :: forall (j :: Bool) (m :: Type) (n :: Type). Proxy j -> m -> n -> If j m n, where If :: forall k. Bool -> k -> k -> k is imported from Data.Type.Bool and is a straightforward conditional choice operator.
  • In the type of x, we see that we need the kind of IfK c b d to match the kind of d. That is, if b :: kappa[3], we have [W] If cb kappa[3] a ~ a. Here, the forall in x's type is at level 3; the RHS of y is at level 2.
  • If we could reduce If cb kappa[3] a to kappa[3], then we would solve kappa[3] := a, but we can't make this reduction, because cb is a skolem.
  • Instead, we finish checking the type of x and promote kappa[3] to kappa[2].
  • Later, we'll make an implication constraint with [G] cb ~ True. When solving that implication constraint, we'll get [W] If True kappa[2] a ~ a and simplify to [W] kappa[2] ~ a, but that will be insoluble because we'll be solving at level 3, and now kappa[2] is at level 2. We're too late.

Yet, I claim that this program should be accepted, and it would be if GHC tracked a set of ambient givens and used them in local calls to the solver. With these "ambient givens" (instead of putting them only in implication constraints), we would know cb ~ True the first time we try to solve, and then we'll succeed.

An alternative story is to change how levels are used with variables. Currently, levels are, essentially, the number of type variables available from an outer scope. Accordingly, we must make sure that the level of a variable is never higher than the ambient level. (If it were, we wouldn't know what extra variable(s) were in scope.) Instead, we could just store the list of variables that were in scope. We wouldn't then need to promote in this case -- promotion would happen only during floating. But tracking these lists is a real pain. (If we decide to pursue this further, I can add more details, but it's all in Chapter 6 in my thesis -- section 6.5 to be specific.)

Change History (14)

comment:1 Changed 4 months ago by simonpj

Here's another idea, IMHO far better than "storing the list of variables in scope".

  • Give every Implication a unique identity. The already have one, in the form of the EvBindsVar (see ebv_uniq), but we should probably promote it to the Implication itself, replacing the ic_tclvl field.
  • Instead of a level, store in a (meta) TcTyVar the identity of its enclosing implication. Call that the implication parent of the TcTyVar.
  • A TcTyVar is touchable iff its implication parent is the current implication.
  • Levels are already immutable; when promoting a tyvar we make a new one, and we can still do that fine.

Implication identities completely replace level numbers.

Now, in the example, we'll give x the type

   x :: forall a (b :: kappa[i34]) (d :: a). SameKind (IfK c b d) d

plus the leftover implication constraint

   forall[i34] a b d. If cb kappa[i34] a ~ a

Here i34 is the identity of the parent implication, which arises from the forall in the type signature.

That implication constraint is emitted unsolved; and x's type is in the environment with this now-forever-untouchable kappa[i34]. It can only be touched (and hence solved) when we have another go at solving that implication constraint -- which we will.

And Bob's your uncle.

comment:2 Changed 4 months ago by simonpj

Keywords: TypeInType added

comment:3 Changed 4 months ago by goldfire

But how do we instantiate the type of x at an occurrence? We'll generate alpha, beta, and delta to instantiate for a, b, and d, respectively. We figured out a while ago that a's kind -- hence alpha's -- is Type. But what will beta's kind be? It can't quite be kappa[i34], because kappa[i34] might turn out to mention a, not alpha. Instead, it has to be kappa[i34][a |-> alpha], as some kind of suspended substitution. My thesis (and Adam's) does this by including a list of variables at every occurrence of a unification variable. Thus, it would be beta_[alpha], where it's understood that alpha is the instantiation of variables that might appear in beta's kind. Similarly, delta would really be delta_[alpha,beta], because delta is preceded by two instantiated variables.

Really, all comment:1 does is to come up with a concise (and very convenient) way to store lists of variables, by naming the lists and storing the names. But I don't think it eliminates all the attendant complication of instantiation.

comment:4 Changed 3 months ago by simonpj

I don't understand your explanation of the problem, but I think I understand the problem you are explaining. Suppose we have

let x :: forall a b (d :: a). SameKind (IfK c b d) d
             x = undefined
         in (x, blah)

I have changed the in part. At the occurrence of x are must instantiate x's type. But x's type currently looks like

 x :: forall (a :: Type) (b :: kappa[i34]) (d :: a). <stuff>

We can instantiate

  a :-> (alpha :: Type)
  d :-> (delta :: alpha)

but what about b?

We can't possibly have b :-> (beta :: kappa[i34])! If we'd solved kappa[i34] := a (which will eventually happen), and done so before instantiating x at its call site, then we'd have instantiated b just like d.

My conclusion: we cannot instantiate any type T from the environment that has any free "internal" unification variables, where by "internal" mean ones that can be unified with type involving the quantified type variables of T.

The current zonkPromote stuff achieves this by promoting such variables; but in exchange typing becomes order-dependent (bad), and cannot (currently) take advantage of "ambient" givens. For the order-dependence, instead of the Refl match, consider something like

f (y::Proxy c) = ( let x :: forall a b (d :: a). SameKind (IfK c b d) d
                       x = undefined
                   in (x, blah)
                 , y :: Proxy True))

Here we discover that c (a unification variable) is True, but only after we've looked at the second component of the pair.

Hmm. All I can think of is to delay the instantiation of x until its type has "settled". That would require us to add instantiation constraints, which we'll want eventually anyway --- impredicative polymorphism certainly requires this, for a very similar reason.

I don't see how your "tyars in scope" thing deals with this at all.

comment:5 Changed 3 months ago by goldfire

The "tyvars in scope" is a red herring. Or, rather, your approach of linking a unification var to its enclosing implication carries the same data, so there is no difference between our approaches.

My comment:3 tersely suggested a way to allow x's instantiation, even before everything has settled. It might be equivalent to your instantiation constraints -- hard to say. (Are these specified in the paper? I don't recall.)

Consider this version:

f (y::Proxy c) = let x :: forall a b (d :: a) z. z -> SameKind (IfK c b d) d
                     x = undefined
                 in (x (y :: Proxy True), blah)

Now, we get the key bit of information -- that c is True -- in an argument passed to x, which we cannot look at without instantiating x. (We need to instantiate x before looking at its arguments because perhaps x is higher-rank and we'll need to "push down" the polymorphic type of x's argument. Indeed, I could have made my example higher-rank to demonstrate this, but didn't for simplicity.) If the instantiation constraints can handle this case, then they're likely equivalent to what I was thinking about in comment:3.

comment:6 Changed 3 months ago by simonpj

Cc: A.SerranoMena@… added

I missed the bit about delayed substitution. Yes, maybe you could do that. It looks like a pretty major complication to me: an entirely new form of type (a delayed substitution) will all the knock-on effects that might ensue.

Instantiation constraints would be less expressive but less drastic. They are described in Guarded impredicative polymorphism (PLDI'18). I'm adding Alejandro in cc.

I'm not sure if the system in that paper could handle the higher rank case of delayed instantiation -- but I think so.

The question remains: what to do in the short term. My instinct: reject the program. We can accept it later, but rejecting now is safe, and can easily be fixed by adding more type annotations. Anything else seems either (a) vulnerable to constraint-solving order or (b) extremely complicated in ill-understood ways.

I think "reject the program" means "reject if any variables would be promoted by zonkPromote".

comment:7 Changed 3 months ago by goldfire

I'm fine with rejecting such programs (if we agree that doing so is a small infelicity). But I'm totally unsure of how to do this.

Your "reject if any variables would be promoted by zonkPromote" is wrong on two counts, I'm afraid:

  1. The program in question in this ticket doesn't use zonkPromote at all -- it goes by way of kindGeneralizeLocal. So let's generalize your proposal to be "reject if any variables would be promoted by zonkPromote or kindGeneralizeLocal".
  1. This proposal would reject too many programs. I replaced the zonkPromoteType with zonkTcType in pattern signatures and found 4 failures in the typecheck directory of the testsuite (should_compile/tc150, should_compile/tc194, should_compile/tc211, and should_fail/tcfail104). Here is tc150:
f v = (\ (x :: forall a. a->a) -> True) id -- 'c'

The RuntimeRep unification variable in the kind of a must be promoted.

The other uses of zonkPromote are similarly necessary for programs that have long been accepted.

On the other hand, it's possible that skipping promotion in kindGeneralizeLocal (and just erroring instead) would work. Promotion there happens when there is a constrained unification variable in a type that we can't solve right away. Perhaps we just don't allow those. Simply skipping the promotion in the testsuite finds breakages (assertion failures) only in programs that we already reject, so this wouldn't lead to a regression.

But on more thought, I don't think this (= don't promote in kindGeneralizeLocal) buys us anything. The goal is to make type checker order-independent. However, this change doesn't do that. In the examples we've been considering, we must take the case where c has been unified both before and after processing x's signature. If c hasn't yet been unified, our new approach will reject x: good. But if c has been unified, the new approach will accept x: bad.

Bottom line: I don't think it's so simple to detect this corner case. And I don't have a better idea right now, short of delayed substitutions.

I don't think the delayed substitutions are really that bad, though. They would not, say, be a new constructor for TcType. Instead, they would only be a feature of MetaTv: any place but a unification variable can apply the substitution. Just about all our algorithms (e.g. unification) have to treat MetaTv specially already. The new treatment would simply apply the substitution as a part of the special processing. I'm not saying there is zero cost here, but that I think the complexity would be localized to MetaTv and functions that already process MetaTv.

comment:8 Changed 3 months ago by simonpj

The goal is to make type checker order-independent. However, this change doesn't do that.

Darn. You are right.

Let's see. Let's think first about kindGeneralizeLocal. There are two cases:

  1. All the lexically-scoped tyvars mentioned in the type were born as skolems. (By "born as skolems" I mean existentials and ones introduced by the 'foralls' of a type signature. This matches my intutition that a type signature should fully specify the type.

In that case I claim that "fail if zonkPromote would promote anything" is absolutely predictable, not order-dependent.

  1. Some lexically-scoped tyvars were born as meta-tyvars. (Example: ones bound by pattern signatures.) In that case we may discover what type they stand for, adn order is important. Comment:4, \(y :: Proxy c). blah is an example. And you are right that if we find out what c is early, we'll solve that If c kappa a ~ a constraint really easily, and will never "see" a problem. So (short term solution, remember) maybe we should reject such programs outright.

I have not yet thought about the non-generalised ones.

For the medium term solution, I'm more inclined to the solution in Guarded impredicative polymorphism, because it's fairly well worked out, and also addresses another problem (impredicativity). I don't have a clear picture of the ramifications of this delayed-substitution thing. (E.g. what does alpha[ beta :-> ty ] ~ ty2 do?) It seems like a very big hammer for a corner case.

Last edited 3 months ago by simonpj (previous) (diff)

comment:9 Changed 3 months ago by goldfire

I think there's a third case: there might be a variable born as a skolem that nevertheless mentions unification variables in its kind. This could happen, for example, with a forall-bound variable in a partial type signature.

I don't see your short-term solution. It sounds like you're saying "forbid lexical meta-tyvars in type signatures" but that's a huge hammer. And it wouldn't even work, because meta-tyvars might be zonked before we can forbid them. Perhaps I'm missing something.

Your medium-term solution might work -- I don't have enough of it in my head to analyze. I took a quick look at the paper (Fig. 7, in particular) and have a question: is the new system fully backward-compatible with "Practical type inference"? Here is an example I'm worried about:

polypoly :: ((forall a. a -> a) -> (Int, Char)) -> ()
polypoly _ = ()

stuff = polypoly (\f -> (f 5, f 'x'))

This is accepted today, right in line with "Practical type inference". But it looks like it wouldn't be accepted by Fig. 7, because that assigns a monotype to any un-annotated lambda. The f above must be assigned a polytype. I have not read the paper (since last summer), but a quick glance at the figure provoked this question.

comment:10 Changed 3 months ago by simonpj

there might be a variable born as a skolem that nevertheless mentions unification variables in its kind.

Rats. Yes, that is true. Also an exisential match on

data T k where
  MkT :: forall (a :: k). blah -> T k

"forbid lexical meta-tyvars in type signatures" but that's a huge hammer.

Yes, that is what I'm saying. Let's review the problem:

  • We can't instantiate a type signature that contains a meta-variable if that meta-variable might later be instantiated to one of the quantified variables of the signature. (Unless we venture in the uncharted waters of delayed substitutions.)
  • If we have solved all the constraints arising from the signature, and any free meta-variables are from an outer level, there is no problem -- outer-level variables can't be solved in a way that mentions the inner quantifiers.
  • But "solving all the constraints" might (in obscure cases) depend on whether or not we have worked out the value of some outer level variable. Thus If alpha[0] beta[1] Int ~ a[1]; if alpha turns out to be True we learn that beta := a.
  • We could reject the obscure situation, but we can't detect when it happens: suppose we unified alpha := True much much earlier and zonked it away.
  • This kind of order-dependence already arises when we use simplifyInfer in NoMonoLocalBinds; here again, an outer alpha[0] might unlock an inner constraint. But with MonoLocalBinds (our well-behaved case), it does not happen.

We'd like a MonoLocalBinds for type signatures, which ensures their good behaviour. But I don't see one, apart from the big hammer of saying that the type can mention only lexically scoped variables whose type and kind are fixed from the moment it comes into scope. (And even that is not a very well-defined statement.)

It's very frustrating that there is no simple way to identify a well-behaved subset.

comment:11 Changed 3 months ago by goldfire

The problem is that you're ruling out several examples in our recent type variables paper.

For example (this doesn't actually appear in the paper, but many similar forms do):

prefix (x :: a) yss = map xcons yss
  where xcons :: [a] -> [a]
        xcons ys = x : ys

Under our recent change to allow patterns to bind meta-tyvars, the type signature here would be rejected. That's really terrible!

One sledgehammer of a solution is to disable the eager unifier. Then, refuse to promote in kindGeneralizeLocal, issuing errors instead. I do think that would exactly fix the problem. We always assume that the eager unifier is good for performance, but have we ever tested this? Perhaps it doesn't!

I still can't help but think that delayed substitutions are the answer here. (The instantiation constraints seem similar. I'm arguing for delayed substitutions only because I've studied them more closely.) Adam used them in his thesis for inference. I thought they were horribly complex and resolutely decided that I would have none of that rubbish in my thesis. Everything went swimmingly without them until I actually tried to write any proofs. And then, bit by bit, all the complexity Adam discovered painstakingly had to enter. I was really quite displeased with it all, wanting something cheap and cheerful instead. But I finished the experience rather convinced that delayed substitutions are the one true way to do this, having been saddled with them when trying quite hard to avoid them.

Perhaps we don't need to implement delayed substitutions directly, if we can come up with a clever implementation trick that's functionally equivalent (like storing implication identities instead of lists of tyvars, noting that the two have equal informational content). Of course, any of this is at least a medium-term solution.

The short-term solution may well be to do nothing (other than fix the panic in #15588, which is hopefully quite superficial -- I haven't looked yet). The status quo means we behave unpredictably in some awfully obscure scenarios. This is unabashedly the wrong thing, but I don't think it's ruining anyone's day but ours. When we infer a type, the type is correct, so there's no safety issue here. I think order-dependence in highly obscure code is better than the huge sledgehammers we've been considering here.

comment:12 Changed 3 months ago by AlejandroSerrano

Indeed, when working in the Guarded impredicativity paper we considered delaying instantiations as a solution, which we rejected because it was quite complicated. Applying that solution to this case, the instantiation of

 x :: forall (a :: Type) (b :: kappa[i34]) (d :: a). <stuff>

would be forbidden until kappa[i34] is known. That entails that d is not instantiated either, as it appears later in the time.

However, in the paper we do not explicitly mention kind signatures. We assume that if we have a quantified type, we can always instantiate its variables -- we only have to choose whether we instantiate them with some restrictions or not. There is some work to be done to ensure that this kind of scenarios doesn't break the invariants for termination of checking.

comment:13 Changed 3 months ago by simonpj

Here's another idea: if a type signature has any free, lexically-scoped type variables, then treat it as a partial type signature, for which we already have elaborate support. Partial type signatures are used to guide and constrain type inference, but NOT used as the single canonical specification of the type of x, nor used to support polymorphic recursion.

That's still annoying: we might want polymorphic recursion, and if so how would we get it. But the point about having free unification variables is that we don't really know the type at all, yet. And that's what partial type signatures are all about.

Last edited 3 months ago by simonpj (previous) (diff)

comment:14 Changed 7 weeks ago by Ningning Xie <xnningxie@…>

In 3905c3c/ghc:

Update core-spec for Coercion Quantification

Summary:
Update details for `ForAllTy` and `ForAllCo` in core-spec, as they
can now quantify over coercion variables.

Test Plan: Please read core-spec.pdf

Reviewers: goldfire, simonpj, bgamari

Reviewed By: goldfire

Subscribers: rwbarton, carter

GHC Trac Issues: #15497, #15589

Differential Revision: https://phabricator.haskell.org/D5247
Note: See TracTickets for help on using tickets.