#15743: Nail down the Required/Inferred/Specified story -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.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 goldfire): Why? Consider {{{#!hs class C b where meth :: a -> b -> b }}} The full type for `meth` is `meth :: forall b. C b => forall a. a -> b -> b`. Note that `b` comes first, even though it is mentioned lexically second in the type of `meth`. I suppose we ''could'' pull the `a` all the way out to the front, but I think the current treatment is nice and predictable. What about {{{#!hs class C2 a b | a -> b where meth2 :: c -> a -> a }}} Using the same reasoning, we get `meth2 :: forall a b. C2 a b => forall c. c -> a -> a`. Note that `b` is Specified in the type of `meth2`. Returning to associated types (and the example from comment:12), we want associated types to behave somewhat like terms. Let's suppose we have Constrained Type Families, as I think that's the right model for all this. Then, we would get `T :: forall {k} (a :: k). C @k a => forall (f :: k -> Type). f a -> Type`. See now nicely that parallels the term-level treatment! Of course, we don't get the `C a` constraint these days, but that leaves us with `forall {k} (a :: k) (f :: k -> Type). f a -> Type`, as suggested by that Note. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15743#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler