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

 The problem is that you're ruling out several examples in our recent type
 variables paper.

 For example (this doesn't actually appear in the paper, but many similar
 forms do):

 {{{#!hs
 prefix (x :: a) yss = map xcons yss
   where xcons :: [a] -> [a]
         xcons ys = x : ys
 }}}

 Under our recent change to allow patterns to bind meta-tyvars, the type
 signature here would be rejected. That's really terrible!

 One sledgehammer of a solution is to disable the eager unifier. Then,
 refuse to promote in `kindGeneralizeLocal`, issuing errors instead. I do
 think that would exactly fix the problem. We always assume that the eager
 unifier is good for performance, but have we ever tested this? Perhaps it
 doesn't!

 I still can't help but think that delayed substitutions are the answer
 here. (The instantiation constraints seem similar. I'm arguing for delayed
 substitutions only because I've studied them more closely.) Adam used them
 in his thesis for inference. I thought they were horribly complex and
 resolutely decided that I would have none of that rubbish in ''my''
 thesis. Everything went swimmingly without them until I actually tried to
 write any proofs. And then, bit by bit, all the complexity Adam discovered
 painstakingly had to enter. I was really quite displeased with it all,
 wanting something cheap and cheerful instead. But I finished the
 experience rather convinced that delayed substitutions are the one true
 way to do this, having been saddled with them when trying quite hard to
 avoid them.

 Perhaps we don't need to implement delayed substitutions directly, if we
 can come up with a clever implementation trick that's functionally
 equivalent (like storing implication identities instead of lists of
 tyvars, noting that the two have equal informational content). Of course,
 any of this is at least a medium-term solution.

 The short-term solution may well be to do nothing (other than fix the
 panic in #15588, which is hopefully quite superficial -- I haven't looked
 yet). The status quo means we behave unpredictably in some awfully obscure
 scenarios. This is unabashedly the wrong thing, but I don't think it's
 ruining anyone's day but ours. When we infer a type, the type is correct,
 so there's no safety issue here. I think order-dependence in highly
 obscure code is better than the huge sledgehammers we've been considering
 here.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15589#comment:11>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler