[GHC] #9858: Typeable instances should be kind-aware

[GHC]

#9858: Typeable instances should be kind-aware
-------------------------------------+-------------------------------------
        Reporter:  dreixel           |                   Owner:
            Type:  bug               |                  Status:  merge
        Priority:  highest           |               Milestone:  7.10.2
       Component:  Compiler          |                 Version:  7.9
      Resolution:                    |                Keywords:
Operating System:  Unknown/Multiple  |            Architecture:
 Type of failure:  None/Unknown      |  Unknown/Multiple
      Blocked By:                    |               Test Case:
 Related Tickets:                    |  typecheck/should_fail/T9858a,
                                     |  should_run/T9858b
                                     |                Blocking:
                                     |  Differential Revisions:  Phab:D652
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Sigh.  `ImpredicativeTypes` certainly causes a lot of pain given that it's
 a feature that doesn't work and is unsupported.

 The problem here is that we should never unify `(c => t)` with `a b`, as
 happens in the call `i (Proxy :: Proxy (Eq Int => Int))`.  Here what
 happens when I fix this:
 {{{
 T9858.hs:24:8: error:
     Couldn't match type `Eq Int => Int' with `a0 b0'
     Expected type: Proxy (a0 b0)
       Actual type: Proxy (Eq Int => Int)
     In the first argument of `i', namely
       `(Proxy :: Proxy (Eq Int => Int))'
     In the expression: i (Proxy :: Proxy (Eq Int => Int))
     In an equation for `j': j = i (Proxy :: Proxy (Eq Int => Int))
 }}}
 And that seems entirely reasonable.

 Thank you  -  you are amazingly good at exposing my inadequate thinking.
 Keep it up!  (Meanwhile I'll plug this hole tomorrow.)

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