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

5 Feb 2015

      #9858: Typeable instances should be kind-aware
-------------------------------------+-------------------------------------
        Reporter:  dreixel           |                   Owner:  dreixel
            Type:  bug               |                  Status:  new
        Priority:  highest           |               Milestone:  7.10.1
       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:                    |                Blocking:
                                     |  Differential Revisions:
-------------------------------------+-------------------------------------

Comment (by goldfire):

 We are certainly not aiming for 100% backward compatibility. Indeed we
 can't -- `unsafeCoerce` compiles today, and we don't want it to compile
 tomorrow. So, at least that program will be omitted. Because of the
 conservative nature of type systems, some more programs will be excluded,
 most likely. We want this extra set to be small, but I'm not overly
 worried about it.

 As for this example:
 {{{
 f :: Proxy (a :: k) -> Proxy (b :: k) -> Proxy (Proxy :: k -> *)
 f _ _ = Proxy

 g pa pb = typeRep (f pa pb)
 }}}

 I get

 {{{
 g (pa :: Proxy <k0> a0) (pb :: Proxy <k1> b0)
   = typeRep <(k2 -> *) -> *>  *) -> *>>  *>>
 <$dict>
             (f <k2> <a1> <b1> pa pb)
   where
     $dict :: Typeable <(k2 -> *) -> *> (Proxy  *>)
 }}}

 Unifying some variables and generalizing gives us

 {{{
 g <k :: BOX> <a :: k> <b :: k> (pa :: Proxy (a :: k)) (pb :: Proxy (b ::
 k))
   = typeRep <(k -> *) -> *>  *) -> *>>  *>>
 <$dict>
             (f <k> <a> <b> pa pb)
   where
     $dict :: Typeable <(k -> *) -> *> (Proxy  *>)
 }}}

 We then generalize over the `Typeable` constraint, giving

 {{{
 g :: forall (k :: BOX) (a :: k) (b :: k).
      Typeable <(k -> *) -> *> (Proxy  *>)
   => Proxy <k> a -> Proxy <k> b -> TypeRep
 }}}

 or, in source Haskell

 {{{
 g :: Typeable (Proxy :: (k -> *) -> *)
   => Proxy (a :: k) -> Proxy (b :: k) -> TypeRep
 }}}

 Again, I don't see the ambiguity, and I think GHC would be able to infer
 this type without trouble... I don't see how this is a special case,
 really.

--
Ticket URL: 
GHC 
The Glasgow Haskell Compiler