Opened 19 months ago

Closed 2 months ago

#11672 closed bug (fixed)

Poor error message

Reported by: adamgundry Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.0.1-rc2
Keywords: TypeErrorMessages, TypeInType Cc: goldfire, diatchki
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Incorrect warning at compile-time Test Case: typecheck/should_fail/T11672
Blocked By: Blocking:
Related Tickets: #11198 Differential Rev(s):
Wiki Page:

Description

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.

Change History (6)

comment:1 Changed 19 months ago by simonpj

Keywords: TypeInType added

comment:2 Changed 13 months ago by RyanGlScott

For reference, here is the current error message in GHC 8.0.1/HEAD:

    • Couldn't match type ‘*’ with ‘Symbol’
      Expected type: Proxy ((->) Int Bool)
        Actual type: Proxy (Int -> Bool)
      Use -fprint-explicit-kinds to see the kind arguments
    • 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))

This seems to address the first and third bullet points above.

comment:3 Changed 7 months ago by adamgundry

Owner: adamgundry deleted

comment:4 Changed 5 months ago by simonpj

Keywords: TypeErrorMessages added; ErrorMessages removed

comment:5 Changed 2 months ago by Richard Eisenberg <rae@…>

In 9a54975/ghc:

Test #11672 in typecheck/should_fail/T11672.

I believe this was fixed with the fix for #11198.

comment:6 Changed 2 months ago by goldfire

Resolution: fixed
Status: newclosed
Test Case: typecheck/should_fail/T11672
Note: See TracTickets for help on using tickets.