#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