[GHC] #11186: Give strong preference to type variable names in scope when reporting hole contexts

[GHC]

#11186: Give strong preference to type variable names in scope when reporting hole
contexts
-------------------------------------+-------------------------------------
        Reporter:  dfeuer            |                Owner:
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.10.2
  checker)                           |
      Resolution:                    |             Keywords:  typed-holes
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):

 OK I understand.  Here is a version of comment:4 that actually shows the
 problem
 {{{
 {-# LANGUAGE ExistentialQuantification, ScopedTypeVariables #-}
 module T11186 where
   data Foop = forall xx . Foop xx
   blah (Foop (q :: pah)) = length ([q] :: _)
 }}}
 We get
 {{{
 T11186.hs:8:41: error:
     • Found type wildcard ‘_’ standing for ‘[xx]’
       Where: ‘xx’ is a rigid type variable bound by
                a pattern with constructor: Foop :: forall xx. xx -> Foop,
                in an equation for ‘blah’
                at T11186.hs:8:7
 }}}
 Now, the difficulty is this: lexically scoped type variable might be bound
 somewhere very different to the existential pattern itself.  For example:
 {{{
 bla2 (Foop q) = (\(r::pah) -> length ([r] :: _)) q
 }}}
 And indeed, the same skolem bound in the pattern might have different
 lexical names in different places:
 {{{
 bla2 (Foop q) = ( (\(r::pah) -> length ([r] :: _)) q
                 , (\(r::hap) -> length ([r] :: _)) q )
 }}}
 Now what would you expect?

 Ugh. Tiresome, and not particularly easy to fix.
  * Visible type application will let you bind the type variable in the
 pattern (which is where it "ought" to be bound

  * Maybe some hack could do a better job when the type variable is in fact
 bound in the pattern where the existential is born.

 Funnily enough, Richard, Stephanie, Adam, and I were discussing questions
 around lexically scoped type variables only last week.

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