#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