[GHC] #13401: GHCi gives conflicting information about visible type application

[GHC]

#13401: GHCi gives conflicting information about visible type application
-------------------------------------+-------------------------------------
        Reporter:  crockeea          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  GHCi              |              Version:  8.0.1
      Resolution:                    |             Keywords:
                                     |  TypeApplications
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #11376, #11975    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * related:   => #11376, #11975


Comment:

 What prompted this is chronicled in #11376 (particularly from
 [https://ghc.haskell.org/trac/ghc/ticket/11376#comment:15 comment:15]
 onward). It was discovered that when `:type` was used with a visibly
 applied type, you could get some weird results, like this one:

 {{{
 λ> import GHC.Generics
 λ> :type datatypeName @('MetaData "Void" "Data.Void" "base" 'False)
 datatypeName @('MetaData "Void" "Data.Void" "base" 'False)
   :: Datatype ('MetaData "Void" "Data.Void" "base" 'False) =>
      forall k1 (t :: Meta -> (k1 -> *) -> k1 -> *) (f :: k1
                                                          -> *) (a :: k1).
      t ('MetaData "Void" "Data.Void" "base" 'False) f a -> [Char]
 }}}

 Before, `:type` was instantiating constraints lazily, which is why that
 `Datatype` constraint is still lingering around in the type that `:type`
 infers above, even though `'MetaData "Void" "Data.Void" "base" 'False`
 should discharge that constraint. simonpj thought this was ghastly and
 changed the behavior of `:type` to //deeply// instantiate the inferred
 type (i.e., solve constraints as much as possible) and re-generalize
 afterwards.

 (Note: "generalize" comes from a rule in Hindley–Milner type inference, I
 believe, where you infer a type of the form `forall a. ...`).

 After this change, you get this instead:

 {{{
 λ> :type datatypeName @('MetaData "Void" "Data.Void" "base" 'False)
 datatypeName @('MetaData "Void" "Data.Void" "base" 'False)
   :: t ('MetaData "Void" "Data.Void" "base" 'False) f a -> [Char]
 }}}

 which is certainly nicer to look at. But it comes at a downside: deep
 instantiation followed by re-generalization can change the visibilities of
 type parameters, which explains the behavior you reported originally in
 this ticket. To work around this, goldfire introduced `:type +v` in
 #11975, which gives you the original lazy instantiation behavior that
 `:type` used to have.

 OK, that ended being a much lengthier explanation that I'd hoped for.
 Hopefully, you understand the context of this a little better. My question
 to you is now: how should we update the users' guide to explain this
 wrinkle? I'm a bit reluctant to include a crash-course on HM type
 inference, but maybe there's an instructive way to give the highlights of
 this discussion to readers.

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