GHC does not rewrite in FunTy
Consider
{-# LANGUAGE ExplicitForAll, PolyKinds, DataKinds, TypeFamilies, GADTs #-}
module Bug where
import GHC.Exts
class C x where
meth :: x -> ()
instance C (a -> b) where
meth _ = ()
type family Lifty throttle where
Lifty Int = LiftedRep
data G a where
MkG :: G Int
foo :: forall i (a :: TYPE (Lifty i)) (b :: TYPE (Lifty i)). G i -> (a -> b) -> ()
foo MkG = meth
GHC rejects, saying it cannot find an instance for C (a -> b)
. But it should accept.
The problem is that the kinds of a
and b
are TYPE (Lifty i)
. Even if we know i ~ Int
, and therefore that Lifty i ~ LiftedRep
, GHC does not rewrite these kinds internally, allowing instance matching to succeed.
!2477 (closed), when complete, should address this.