#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