Opened 5 years ago

Closed 5 years ago

#10054 closed bug (fixed)

Misleading error message from unsaturated type family application

Reported by: sherman Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.8.3
Keywords: type families, constraint kinds Cc:
Operating System: MacOS X Architecture: x86_64 (amd64)
Type of failure: Incorrect warning at compile-time Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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.

Change History (1)

comment:1 Changed 5 years ago by rwbarton

Resolution: fixed
Status: newclosed

Thanks for the report. As you correctly diagnosed, the program is invalid due to the undersaturated type family application in Foo (Ap Show) a. The fact that GHC does not report this error (and subsequently gets confused) was a regression introduced somewhere in the 7.8 line, but was fixed in 7.8.4.

rwbarton@morphism:/tmp$ ghc-7.8.1 Test
[1 of 1] Compiling Main             ( Test.hs, Test.o )

Test.hs:12:9:
    Type synonym ‘Ap’ should have 2 arguments, but has been given 1
    In the type signature for ‘test’:
      test :: Ap Show a => Foo (Ap Show) a
rwbarton@morphism:/tmp$ ghc-7.8.3 Test
[1 of 1] Compiling Main             ( Test.hs, Test.o )

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
rwbarton@morphism:/tmp$ ghc-7.8.4 Test
[1 of 1] Compiling Main             ( Test.hs, Test.o )

Test.hs:12:9:
    Type synonym ‘Ap’ should have 2 arguments, but has been given 1
    In the type signature for ‘test’:
      test :: Ap Show a => Foo (Ap Show) a
Note: See TracTickets for help on using tickets.