[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 simonpj):

 > 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.

 and

 > Sadly, we don't allow implicit quantification in the middle of a type,
 saying that all implicit quantification must occur directly after the ::.

 Both these comments about the same thing: if I write an explicit kind
 signature (for a type constructor) or type signature (for a function), can
 the Inferred variables be interleaved with the Specified forall'd ones?
 That indeed seems tricky: after all, the user is explicitly specifying the
 telescope, and we'd have to "insert a variable in that telescope that
 isn't there".

 But I feel similarly about `T` in comment:1 where you propose to insert an
 Inferred `d::k` in the middle of the user-specfied telescope.

 One thing we have not discussed, but perhaps which goes without saying,
 is this: an explicit, user-specified kind signature may specify a
 different order for the Specified variables than the one we'd infer -- and
 then we'd better follow the order in the signature.

 And that leads back to the question: ''is it even possible to specify the
 position of an inferred variable other than at the front?''  Presumably
 not -- if we specified that variable it's be Specified not Inferred!

 So at the moment, pending further debate, I feel pretty strongly that
 Inferred should be at the front, always.

 Overall, my current vote is (1).  It is simple to specify: Inferred, then
 Specified, then Required.  If it becomes irksome we can loosen up.  When
 things get complicated I worry that we might find that our sophisticated
 inference system is incompatible with something we want to do in the
 future.

 Let's keep it simple.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15743#comment:8>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler