#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 goldfire): I'm fine with rejecting such programs (if we agree that doing so is a small infelicity). But I'm totally unsure of how to do this. Your "reject if any variables would be promoted by `zonkPromote`" is wrong on two counts, I'm afraid: 1. The program in question in this ticket doesn't use `zonkPromote` at all -- it goes by way of `kindGeneralizeLocal`. So let's generalize your proposal to be "reject if any variables would be promoted by `zonkPromote` or `kindGeneralizeLocal`". 2. This proposal would reject too many programs. I replaced the `zonkPromoteType` with `zonkTcType` in pattern signatures and found 4 failures in the `typecheck` directory of the testsuite (`should_compile/tc150`, `should_compile/tc194`, `should_compile/tc211`, and `should_fail/tcfail104`). Here is `tc150`: {{{ f v = (\ (x :: forall a. a->a) -> True) id -- 'c' }}} The `RuntimeRep` unification variable in the kind of `a` must be promoted. The other uses of `zonkPromote` are similarly necessary for programs that have long been accepted. On the other hand, it's possible that skipping promotion in `kindGeneralizeLocal` (and just erroring instead) would work. Promotion there happens when there is a constrained unification variable in a type that we can't solve right away. Perhaps we just don't allow those. Simply skipping the promotion in the testsuite finds breakages (assertion failures) only in programs that we already reject, so this wouldn't lead to a regression. But on more thought, I don't think this (= don't promote in `kindGeneralizeLocal`) buys us anything. The goal is to make type checker order-independent. However, this change doesn't do that. In the examples we've been considering, we must take the case where `c` has been unified both before and after processing `x`'s signature. If `c` hasn't yet been unified, our new approach will reject `x`: good. But if `c` ''has'' been unified, the new approach will accept `x`: bad. Bottom line: I don't think it's so simple to detect this corner case. And I don't have a better idea right now, short of delayed substitutions. I don't think the delayed substitutions are really that bad, though. They would not, say, be a new constructor for `TcType`. Instead, they would only be a feature of `MetaTv`: any place but a unification variable can apply the substitution. Just about all our algorithms (e.g. unification) have to treat `MetaTv` specially already. The new treatment would simply apply the substitution as a part of the special processing. I'm not saying there is zero cost here, but that I think the complexity would be localized to `MetaTv` and functions that already process `MetaTv`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15589#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler