#15743: Nail down the Required/Inferred/Specified story -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | dependent/should_fail/T15743[cd], | dependent/should_compile/T15743{,e}, | ghci/scripts/T15743b Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * testcase: => dependent/should_fail/T15743[cd], dependent/should_compile/T15743{,e}, ghci/scripts/T15743b * status: new => closed * resolution: => fixed Comment: The design decisions are written in {{{ {- Note [Required, Specified, and Inferred for types] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We have some design choices in how we classify the tyvars bound in a type declaration. (Here, I use "type" to refer to any TyClDecl.) Much of the debate is memorialized in #15743. This Note documents the final conclusion. First, a reminder: * a Required argument is one that must be provided at every call site * a Specified argument is one that can be inferred at call sites, but may be instantiated with visible type application * an Inferred argument is one that must be inferred at call sites; it is unavailable for use with visible type application. Why have Inferred at all? Because we just can't make user-facing promises about the ordering of some variables. These might swizzle around even between minor released. By forbidding visible type application, we ensure users aren't caught unawares. See also Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in TyCoRep. When inferring the ordering of variables (that is, for those variables that he user has not specified the order with an explicit `forall`) we use the following order: 1. Inferred variables from an enclosing class (associated types only) 2. Specified variables from an enclosing class (associated types only) 3. Inferred variables not from an enclosing class 4. Specified variables not from an enclosing class 5. Required variables before a top-level :: 6. All variables after a top-level :: If this ordering does not make a valid telescope, we reject the definition. This idea is implemented in the generalise function within kcTyClGroup (for declarations without CUSKs), and in kcLHsQTyVars (for declarations with CUSKs). Note that neither definition worries about point (6) above, as this is nicely handled by not mangling the res_kind. (Mangling res_kinds is done *after* all this stuff, in tcDataDefn's call to tcDataKindSig.) We can easily tell Inferred apart from Specified by looking at the scoped tyvars; Specified are always included there. One other small open question here: how to classify variables from an enclosing class? Here is an example: class C (a :: k) where type F a In the kind of F, should k be Inferred or Specified? Currently, we mark it as Specified, as we can commit to an ordering, based on the ordering of class variables in the enclosing class declaration. If k were not mentioned in the class head, then it would be Inferred. The alternative to this approach is to make the Inferred/Specified distinction locally, by just looking at the declaration for F. This lowers the availability of type application, but makes the reasoning more local. However, this alternative also disagrees with the treatment for methods, where all class variables are Specified, regardless of whether or not the variable is mentioned in the method type. A few points of motivation for the ordering above: * We put the class variables before the local variables in a nod to the treatment for class methods, where class variables (and the class constraint) come first. While this is an unforced design decision, it never rejects more declarations, as class variables can never depend on local variables. * We rigidly require the ordering above, even though we could be much more permissive. Relevant musings are at https://ghc.haskell.org/trac/ghc/ticket/15743#comment:7 The bottom line conclusion is that, if the user wants a different ordering, then can specify it themselves, and it is better to be predictable and dumb than clever and capricious. I (Richard) conjecture we could be fully permissive, allowing all classes of variables to intermix. We would have to augment ScopedSort to refuse to reorder Required variables (or check that it wouldn't have). But this would allow more programs. See #15743 for examples. Interestingly, Idris seems to allow this intermixing. The intermixing would be fully specified, in that we can be sure that inference wouldn't change between versions. However, would users be able to predict it? That I cannot answer. Test cases (and tickets) relevant to these design decisions: T15591* T15592* T15743* -} }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15743#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler