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