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 |