[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 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