#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):
{{{
f = \(p :: Proxy Proxy) -> typeRep p
}}}
More fun test cases!
Let's see what GHC will do. First, we must insert kind unification
variables:
{{{
Proxy :: forall (k :: BOX). k -> *
typeRep :: forall (k :: BOX) (proxy :: k -> *) (a :: k).
Typeable <k> a => proxy a -> TypeRep
f = \(p :: Proxy *> (Proxy <k0>)) ->
typeRep *> *>> <$dict> p
where
$dict :: Typeable *> (Proxy <k0>)
}}}
We find that `k0` isn't affected by any equality constraints, and so it
can be generalized over. We can also generalize over the `Typeable`
constraint:
{{{
f :: forall (k :: BOX). Typeable *> (Proxy <k>) => Proxy *>
(Proxy <k>) -> TypeRep
}}}
In surface syntax, this looks like
{{{
f :: Typeable (Proxy :: k -> *) => Proxy (Proxy :: k -> *) -> TypeRep
}}}
Looks fine to me. Am I missing something? I agree that the solver can't
decompose the `Proxy <k>` argument, but that should be OK. Finding
`Typeable` instances (or `Kindable` instances) doesn't involve search, so
GHC can look for the "`Kindable`" without decomposing first. If the
`Kindable` isn't there, no decomposition.
--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9858#comment:51
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler
