Poor error message

Daniel Díaz recently pointed out a particularly terrible error message. Here's a reduced example:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
module BadError where

import GHC.TypeLits
import Data.Proxy

f :: Proxy (a :: Symbol) -> Int
f _ = f (Proxy :: Proxy (Int -> Bool))

With GHC 8.0 RC2, this leads to the following error:

    • Expected kind ‘Proxy ((->) Int Bool)’,
        but ‘Data.Proxy.Proxy :: Proxy (Int -> Bool)’ has kind ‘Proxy
                                                                  (Int -> Bool)’
    • In the first argument of ‘f’, namely
        ‘(Proxy :: Proxy (Int -> Bool))’
      In the expression: f (Proxy :: Proxy (Int -> Bool))
      In an equation for ‘f’: f _ = f (Proxy :: Proxy (Int -> Bool))

or with -fprint-explicit-kinds -fprint-explicit-coercions:

    • Expected kind ‘Proxy
                       Symbol
                       (((->) |> <*>_N -> <*>_N -> U(hole:{aCy}, *, Symbol)_N) Int Bool)’,
        but ‘(Data.Proxy.Proxy) @ k_aCv @ t_aCw ::
               Proxy (Int -> Bool)’ has kind ‘Proxy * (Int -> Bool)’

As Iavor, Richard and I discussed, this message has at least three separate problems:

• It says kind when it should say type.
• ((->) Int Bool) is printed instead of Int -> Bool (because there is a coercion hiding in the type).
• The real error is the insoluble constraint Symbol ~ *, which is not reported at all!

The first two should be fairly easy to fix. For the third, when reporting insoluble constraints, we should prefer to report those on which no other constraints depend. (In this case, the presence of hole:{aCy} in the constraint is an explicit dependency on the other constraint.)

I'll try to take a look at this. It is no doubt related to #11198.

Trac metadata

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