[GHC] #14662: Partial type signatures + mutual recursion = confusion

[GHC]

#14662: Partial type signatures + mutual recursion = confusion
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.2
      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 goldfire):

 OK. I see why polymorphic recursion is no good. But then can you explain
 Example 6? That's polymorphically recursive and is accepted. (It's
 accepted because the "use `SigTv`s" rule for partial type signatures only
 works at the outermost level; nested `forall`s don't benefit.)

 The reason I dislike `SigTv`s is this: When a user writes down a type
 variable, do they mean it to be unique (skolem) with a unique binding
 site, or could it stand for something else (a `TauTv`)? We generally
 choose the former, but wildcards are the latter. These positions are all
 good. But a `SigTv` is something in between: it's a type variable that can
 stand only for another type variable. Does it have a binding site? If yes,
 then what if we discover that it stands for something else? If no, then
 why do we say `forall a` to introduce them (in the case of partial type
 signatures)? The whole thing seems very squishy to me.

 I ''do'' understand why they came into being, and I agree that they solve
 real problems. But I think you'd have a hard time of writing a declarative
 specification of type inference that involves them.

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