#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