#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

#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): See also GhcKinds/KindInference/Examples for some thoughts on how we should behave. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15743#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | -------------------------------------+------------------------------------- Changes (by goldfire): * cc: xnning (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15743#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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): This is still not really working out to my satisfaction. Let's reconsider my example from comment:1. {{{#!hs 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) }}} To get this to be accepted, we must infer this order for the tyvars of `T`, using `@` to denote Specified and `@{..}` to denote Inferred: `k @{d} c a b x`. Note that an Inferred comes after a Required. I'm confident that we can come up with an algorithm to do this. I'm even somewhat confident that the algorithm will be well-specified (including ScopedSort in its specification). However, what if we rewrite this to become {{{#!hs data T' :: forall k (c :: k) (a :: Proxy c) (b :: _) (x :: SimilarKind a b) -> Type }}} Really, `T'` and `T` should be treated the same. Yet to accept `T'`, we would have to insert a variable in that telescope that isn't there. Here's another example worth pondering here, from #14880: {{{#!hs data Foo (x :: Type) :: forall (a :: x). Proxy a -> Type quux :: forall arg. Proxy (Foo arg) -> () }}} We get `Foo :: forall (x :: Type) -> forall (a :: x). Proxy a -> Type`. In the type of `quux`, when we say `Proxy (Foo arg)`, GHC needs to add the implicit application to some variable `alpha` -- otherwise, the implicit kind argument to `Proxy` would have to have a `forall` in it, and that would be impredicative. So we have `quux :: forall arg. Proxy (Foo arg @alpha) -> ()`. The type of `alpha` must be `arg`, but `alpha` is otherwise unconstrained. The polite thing to do would be to quantify over `alpha`, but the only way to do so is to quantify it ''after'' `arg`, thusly: `quux :: forall (arg :: Type) {a :: arg}. Proxy (Foo arg @a) -> ()`. Sadly, we don't allow implicit quantification in the ''middle'' of a type, saying that all implicit quantification must occur directly after the `::`. So, instead of quantifying `alpha`, we zap it to `Any`, yielding `quux :: forall (arg :: Type). Proxy (Foo arg @Any) -> ()`, which is probably not what the user wants, anyway. This is relevant here because the action in `quux` is just like the action in `T'`: both require inserting an implicit quantification in the ''middle'' of a telescope. Also of interest: both `T'` and `quux` are accepted in Idris, with implicit quantification arising the middle of telescopes. (`T` is syntactically not allowed.) I see a few options here (when I say "allow `quux`, I mean to quantify over `alpha` instead of zap it): 1. Disallow all of these declarations. This makes us less powerful than Idris, but it's internally consistent. 2. Allow `T` but not the others. This means that we can insert variables into a list of tyvarbinders in a type/class declaration, but not in a `forall`. 3. Allow `T` and `T'` but not `quux`. This means that we special-case `forall`s in the return kind of type/class declarations to allow variable insertion in the middle of telescopes. 4. Allow them all. The rule for things like `quux` is that we allow insertion of implicit variables into ''top-level'' quantification only, but not necessarily immediately after the `::`. Note that top-level quantification is already special, in that it brings `ScopedTypeVariables` into scope, while inner quantifications do not. As a further experiment, I tried `quux2 : Int -> ({arg : _} -> Proxy (Foo arg)) -> Int` in Idris, to see if it was clever enough to figure this out in a higher-rank situation. Idris said `No such variable arg`. I think this is because it tried to quantify `alpha` at top-level, which is ill- scoped. So I think sticking to top-level implicit quantification is fine. Options 1-3 have a similar implementation cost. (You might think that all the variable swizzling is hard to implement. It's not particularly bad, and we have to do it anyway to attack #15591 and #15592 satisfactorily.) Note that higher-numbered options require less work to generate sensible error messages, which is non-trivial here. Option 4 is a bit worse because of the way the AST stores implicit quantification of variable declarations. I don't think it would be too bad, though. I'm really torn between these options. Probably (1) is the safest territory, but it irks me not to accept these other programs (short of `quux`), when they have truly unambiguous, well specified meanings, and it's not hard to write an algorithm to accept them. I don't like (2) because it shouldn't have to matter where I put the `::`. And (3) shows up a jarring inconsistency between the meaning of `forall` in type/class declarations and variable declarations. Looking forward to hearing your thoughts (for any instantiation of "you"). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15743#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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):

is it even possible to specify the position of an inferred variable other than at the front?

It isn't possible to specify the position of an inferred variable. Full stop. (At least, not until we have explicit specificity.) But this isn't just about Inferred variables. It's also about Specified ones. Here's a slight tweak to `T`: {{{#!hs data T k (c :: k) (a :: Proxy c) (b :: Proxy d) (x :: SimilarKind a b) }}} I've given `b` a kind that mentions `d`. This makes `d` Specified. But poor `d` still must come ''after'' `k`. We can still go ahead with option (1) (which is what I've been reluctantly leaning toward as well), but I'm clarifying here that the problem isn't just with Inferred. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15743#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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): See #15788 for another test case, this time in the process of generalizing a data constructor. (That bug is in the context of visible kind application, but the visible kind application is somewhat incidental in that ticket.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15743#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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

#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