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

 > 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