Misleading error message from unsaturated type family application

This program

{-# LANGUAGE GADTs, ConstraintKinds, KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}

import GHC.Exts (Constraint)

data Foo :: (* -> Constraint) -> * -> * where
  MkFoo :: c a => Foo c a

type family Ap (f :: * -> Constraint) (x :: *) :: Constraint where
  Ap f x = f x

test :: Ap Show a => Foo (Ap Show) a
test = MkFoo

yields the following error message:

[1 of 1] Compiling Main             ( Test.hs, interpreted )

Test.hs:13:8:
    Could not deduce (Ap Show a) arising from a use of ‘MkFoo’
    from the context (Ap Show a)
      bound by the type signature for
                 test :: (Ap Show a) => Foo (Ap Show) a
      at Test.hs:12:9-36
    Relevant bindings include
      test :: Foo (Ap Show) a (bound at Test.hs:13:1)
    In the expression: MkFoo
    In an equation for ‘test’: test = MkFoo
Failed, modules loaded: none.

I have a hypothesis as to why this error occurs. Because the application of Ap in Ap Show a is fully applied in the context, it reduces to the constraint Show a. However, when error messages describe the typeclass context, they don't reduce type synonyms or type families. However, the Ap Show a that cannot be deduced, despite appearing like a saturated application of Ap, must not be due to the fact that the Ap Show in the argument to the Foo type constructor is partially applied.

If the definition of Ap is eta-reduced, the program in fact successfully typechecks. Or, if the result type of test is instead specified as Foo Show a, the program successfully typechecks. If the type variable a is specialized to a concrete type with a Show instance such as Int, the misleading error message still occurs, with Int substituted for a.

I am wondering if there might be some way to report the error in a way that brings attention to the fact that the compiler cannot figure out what Ap Show a is as the constraint that cannot be deduced.

Trac metadata

Trac field	Value
Version	7.8.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture