[GHC] #15743: Nail down the Required/Inferred/Specified story

[GHC]

#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