#11506: uType_defer can defer too long -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: 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): It's more than solver engineering. A pretty fundamental assumption is that a user-writen type signature (at least one without wildcards) specifies a ''fully-defined'' type. No unification variables; a fully defined type. Not necessarily closed; e.g. here the type sig for 'g' is fully defined although it mentions 'a': {{{ f :: forall a. blah f x = let g :: a -> a g x = x in ... }}} But pattern signatures threaten this happy story. They bring into scope a type variable as a name for a type that may not yet be fully defined, and certainly isn't here. Much simpler situations can do this too: {{{ f (x::a, b) = let g :: a -> a g = ... in ... }}} Here `a` will end up being the name of a unification variable. This hasn't caused trouble before, but now it is. If we switched off on- the-fly unification, and did everything in the solver, I bet a lot more instances would pop up. What's irritating is that the ability to name unification variables (or type variables with as-yet-unknown kinds) is not really sought. It's just hard to exclude. One possible solution would be to make pattern signatures do matching (not unification) with the "expected" type, and then insist that the scoped type variable matched a skolem. Another would be to treat type variables bound in this way more like wildards. If we have {{{ f :: _ -> Maybe _ or <expression> :: _ -> Int }}} then we use ''inference'' not checking, and simply use the signature as a "shape" against which the inferred type is matched. So a type signature with any wildcards is NOT treated as a fully defined type. Maybe a type signature with a free type variable bound by a pattern signature should be treated similarly. The machinery to do so is all there now. Uggle. I doubt I'll get to this quickly. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11506#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler