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
, whereIf :: forall k. Bool -> k -> k -> k
is imported fromData.Type.Bool
and is a straightforward conditional choice operator.
- In the type of
x
, we see that we need the kind ofIfK c b d
to match the kind ofd
. That is, ifb :: kappa[3]
, we have[W] If cb kappa[3] a ~ a
. Here, theforall
inx
's type is at level 3; the RHS ofy
is at level 2.
- If we could reduce
If cb kappa[3] a
tokappa[3]
, then we would solvekappa[3] := a
, but we can't make this reduction, becausecb
is a skolem.
- Instead, we finish checking the type of
x
and promotekappa[3]
tokappa[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 nowkappa[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
comment:2 Changed 4 months ago by
Keywords: | TypeInType added |
---|
comment:3 Changed 4 months ago by
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
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
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
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
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:
- The program in question in this ticket doesn't use
zonkPromote
at all -- it goes by way ofkindGeneralizeLocal
. So let's generalize your proposal to be "reject if any variables would be promoted byzonkPromote
orkindGeneralizeLocal
".
- This proposal would reject too many programs. I replaced the
zonkPromoteType
withzonkTcType
in pattern signatures and found 4 failures in thetypecheck
directory of the testsuite (should_compile/tc150
,should_compile/tc194
,should_compile/tc211
, andshould_fail/tcfail104
). Here istc150
:
f v = (\ (x :: forall a. a->a) -> True) id -- 'c'
The
RuntimeRep
unification variable in the kind ofa
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
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:
- 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.
- 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 whatc
is early, we'll solve thatIf 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.
comment:9 Changed 3 months ago by
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
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]
; ifalpha
turns out to beTrue
we learn thatbeta := 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
inNoMonoLocalBinds
; here again, an outeralpha[0]
might unlock an inner constraint. But withMonoLocalBinds
(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
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
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
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.
Here's another idea, IMHO far better than "storing the list of variables in scope".
Implication
a unique identity. The already have one, in the form of the EvBindsVar (seeebv_uniq
), but we should probably promote it to theImplication
itself, replacing theic_tclvl
field.TcTyVar
is touchable iff its implication parent is the current implication.Implication identities completely replace level numbers.
Now, in the example, we'll give
x
the typeHere
i34
is the identity of the parent implication, which arises from theforall
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.