Coercion prevents type family equation from applying
GHC rejects this program:
{-# LANGUAGE ExplicitForAll, PolyKinds, StandaloneKindSignatures,
TypeFamilies, DataKinds #-}
module Bug where
import Data.Kind
type F :: Type -> Type
type family F k where
F k = Type
type family G a where
forall (k :: Type) (a :: Type -> F k) (b :: Type). G (a b, k) = Char
x :: G (Maybe Int, Bool)
x = 'y'
It would be accepted if the a
were missing its kind signature in the equation for G
.
The problem is that we end up with a template like ((a b) |> co, k)
, and GHC's matcher does not know how to propagate a coercion that casts the result of an application.