[GHC] #10054: Misleading error message from unsaturated type family application

[GHC]

#10054: Misleading error message from unsaturated type family application
-------------------------------------+-------------------------------------
              Reporter:  sherman     |             Owner:
                  Type:  bug         |            Status:  new
              Priority:  normal      |         Milestone:
             Component:  Compiler    |           Version:  7.8.3
  (Type checker)                     |  Operating System:  MacOS X
              Keywords:  type        |   Type of failure:  Incorrect
  families, constraint kinds         |  warning at compile-time
          Architecture:  x86_64      |        Blocked By:
  (amd64)                            |   Related Tickets:
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------
 This program

 {{{#!hs
 {-# 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.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10054>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler