[GHC] #11506: uType_defer can defer too long

[GHC]

#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