#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