#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): Here is the defining property of `Specified`: * All specified arguments have a predictable order. In other words, this order is stable regardless of what GHC's solver does. As long as we can uphold that property, then we're free to label variables as Specified. Furthermore, the place where we put Inferred variables is never important and needn't be specified. Accordingly, we can relax a few restrictions in Simon's description. I propose this algorithm instead: 1. Perform kind inference, getting a fully-settled kind for each variable. This process may introduce new kind variables we would like to quantify over. The precise process is beyond the scope of this ticket. 2. Put the variables in this order: first the newly-quantified variables never written by the user (the Inferred ones), in any order; then the Specified ones in order of first lexical occurrence, reading left-to- right; then the Required ones, in their left-to-right order. 3. Sort all these variables according to ''ScopedSort''. If ''ScopedSort'' tries to move one Required variable past another, fail. This new way of treating the variables relaxes two restrictions imposed above: that a Specified can never appear after a Required, and that an Inferred can never appear after a Specified. Here is an example: {{{ data SimilarKind :: forall (c :: k) (d :: k). Proxy c -> Proxy d -> Type data T k (c :: k) (a :: Proxy c) b (x :: SimilarKind a b) }}} We will want to quantify over `b`'s kind (call it `Proxy d`), but that kind depends on the Required `k`. Simon's approach would reject (where? it doesn't say) because we put Inferred before Specified before Required. But my approach will infer {{{ T :: forall (k :: Type) -> forall {d :: k}. forall (c :: k) (a :: Proxy c) (b :: Proxy d) -> SimilarKind a b -> Type }}} Note that `d` comes after `k`. This declaration is rejected today, whether or not we write down `b`'s kind explicitly. I had been loathe to allow such mixed quantification in the past, but now that the algorithm is written down (and can be included in the manual), I feel comfortable doing it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15743#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler