#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