#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