[GHC] #15589: Always promoting metavariables during type inference may be wrong
#15589: Always promoting metavariables during type inference may be wrong -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- 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 {{{#!hs {-# 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 [https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1074&context=compsci_pubs my thesis] -- section 6.5 to be specific.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15589 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15589: Always promoting metavariables during type inference may be wrong -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15589#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15589: Always promoting metavariables during type inference may be wrong -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => TypeInType -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15589#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15589: Always promoting metavariables during type inference may be wrong -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15589#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15589: Always promoting metavariables during type inference may be wrong -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15589#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15589: Always promoting metavariables during type inference may be wrong -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15589#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15589: Always promoting metavariables during type inference may be wrong -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * cc: A.SerranoMena@… (added) Comment: 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 [https://www.microsoft.com/en-us/research/publication /guarded-impredicative-polymorphism/ 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". -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15589#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15589: Always promoting metavariables during type inference may be wrong -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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`". 2. 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`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15589#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15589: Always promoting metavariables during type inference may be wrong -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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.) In that case I claim that "fail if zonkPromote would promote anything" is absolutely predictable, not order- dependent. 2. 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 [https://www.microsoft.com/en-us/research/publication/guarded- impredicative-polymorphism/ 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15589#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15589: Always promoting metavariables during type inference may be wrong -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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: {{{#!hs 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15589#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15589: Always promoting metavariables during type inference may be wrong -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15589#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15589: Always promoting metavariables during type inference may be wrong -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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): {{{#!hs 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15589#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15589: Always promoting metavariables during type inference may be wrong -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15589#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15589: Always promoting metavariables during type inference may be wrong -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Here's another idea: if a type signature has any free, lexically-scoped type variables, then treat it like a ''partial'' type signature. That is, 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15589#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15589: Always promoting metavariables during type inference may be wrong
-------------------------------------+-------------------------------------
Reporter: goldfire | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone: 8.6.1
Component: Compiler | Version: 8.4.3
Resolution: | Keywords: TypeInType
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Ningning Xie
participants (1)
-
GHC