[GHC] #14722: Error message points to wrong location

[GHC]

#14722: Error message points to wrong location
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:  (none)
               Type:  feature        |            Status:  new
  request                            |
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.5
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  Incorrect
  Unknown/Multiple                   |  error/warning at compile-time
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 This rightly fails, but I have an issue with the error message. I think
 points to the visible type application eagerly.. rather than the type
 annotation `(f_xx :: ())`.

 {{{#!hs
 {-# Language RankNTypes, PolyKinds, GADTs, TypeApplications,
 ScopedTypeVariables #-}

 import Data.Kind

 newtype Limit :: (k -> Type) -> Type where
   Limit :: (forall xx. f xx) -> Limit f

 foo :: forall f a. Limit f -> f a
 foo (Limit (f_xx :: ())) = f_xx @a
 }}}

 gives

 {{{
 $ ghci -ignore-dot-ghci /tmp/Test.hs
 GHCi, version 8.5.20180105: http://www.haskell.org/ghc/  :? for help
 [1 of 1] Compiling Main             ( /tmp/Test.hs, interpreted )

 /tmp/Test.hs:9:28: error:
     • Cannot apply expression of type ‘()’
       to a visible type argument ‘a’
     • In the expression: f_xx @a
       In an equation for ‘foo’: foo (Limit (f_xx :: ())) = f_xx @a
   |
 9 | foo (Limit (f_xx :: ())) = f_xx @a
   |                            ^^^^^^^
 Failed, no modules loaded.
 Prelude>
 }}}

 I would have expected:

 {{{
 /tmp/Test.hs:9:13: error:
     • Couldn't match expected type ‘()’ with actual type ‘f xx0’
     • When checking that the pattern signature: ()
         fits the type of its context: forall (xx :: k1). f xx
       In the pattern: f_xx :: ()
       In the pattern: Limit (f_xx :: ())
     • Relevant bindings include
         foo :: Limit f -> f a (bound at /tmp/Test.hs:9:1)
 }}}

 Thoughts

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