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