[GHC] #15589: Always promoting metavariables during type inference may be wrong

[GHC]

#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