Opened 13 months ago

Last modified 13 months ago

#16050 new feature request

Instance resolution error message unclear, because of missing kind information

Reported by: chessai Owned by: chessai
Priority: normal Milestone:
Component: Compiler Version: 8.6.3
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #13992, #14146 Differential Rev(s):
Wiki Page:

Description

consider the following modules:

module A where

(.) :: forall (a :: TYPE 'UnliftedRep) (b :: TYPE 'UnliftedRep) (c :: TYPE 'UnliftedRep).
     (b -> c)
  -> (a -> b)
  -> (a -> c)
(.) f g = \x -> f (g x)

data UList (a :: TYPE 'UnliftedRep) where
  UNil :: UList a
  UCons :: a -> UList a -> UList a

mapFB :: forall (a :: TYPE 'UnliftedRep)
                (elt :: TYPE 'UnliftedRep)
                (lst :: Type).
  (elt -> lst -> lst) -> (a -> elt) -> a -> lst -> lst
mapFB c f = \x ys -> c (f x) ys

{-# RULES
"mapFB" forall c f g. mapFB (mapFB c f) g = mapFB c (f . g)
   #-}
module B where

import Control.Category ((.))

data UList (a :: TYPE 'UnliftedRep) where
  UNil :: UList a
  UCons :: a -> UList a -> UList a

mapFB :: forall (a :: TYPE 'UnliftedRep)
                (elt :: TYPE 'UnliftedRep)
                (lst :: Type).
  (elt -> lst -> lst) -> (a -> elt) -> a -> lst -> lst
mapFB c f = \x ys -> c (f x) ys

{-# RULES
"mapFB" forall c f g. mapFB (mapFB c f) g = mapFB c (f . g)
   #-}

Module 'A' works fine. Module 'B', fails with the following error:

     No instance for (Category (->)) arising from a use of .
     In the second argument of mapFB, namely (f . g)
      In the expression: mapFB c (f . g)
      When checking the transformation rule "mapFB"
    |
line| "mapFB" forall c f g. mapFB (mapFB c f) g = mapFB c (f . g)
    |                                                      ^^^

I expected this failure because of the kind mismatch; the category instance for (->) obviously requires that it be kinded Type -> Type -> Type. However, it confused someone I am teaching, who said to me that they didn't understand the error, since they expected it to work as (->) does indeed have a Category instance. (They are very unfamiliar with Levity-Polymorphism).

My question is this: Would it be preferable to include such kind information in the error message?

Change History (7)

comment:1 Changed 13 months ago by chessai

Now that I think of this, this confused me a lot more the first time I came across such an error. The error message just says nothing about the kinds, so saying that an instance doesn't exist is pretty confusing.

comment:2 Changed 13 months ago by simonpj

I agree.

For equality mis-matches, GHC already tries not to report T Int does not match T Int, by seeing if the only differences are in the kinds. (The logic is in TcErrors.pprWithExplicitKindsWhenMismatch.)

It would be tiresome, but not hard, to do the same for instance matching, printing the kinds if the only reason for the lack of a match is in the kinds.

Any volunteers?

comment:3 Changed 13 months ago by RyanGlScott

comment:4 Changed 13 months ago by chessai

Owner: set to chessai

I can work on this.

comment:5 Changed 13 months ago by RyanGlScott

(The related tickets were removed for some mysterious reason.)

comment:6 Changed 13 months ago by monoidal

This looks to be the same problem, but for equality:

{-# LANGUAGE GADTs, TypeOperators, PolyKinds #-}

import GHC.Types

data a :~: b where Refl :: a :~: a

foo :: TYPE a :~: TYPE b
foo = Refl

gives an error message

    • Couldn't match type ‘'LiftedRep’ with ‘'LiftedRep’
      ‘a’ is a rigid type variable bound by
        the type signature for:
          foo :: * :~: *
        at Repr.hs:7:1-24
      ‘b’ is a rigid type variable bound by
        the type signature for:
          foo :: * :~: *
        at Repr.hs:7:1-24

To see the problem, you need to use -fprint-explicit-runtime-reps. (I'm not sure if this should be a separate ticket.)

comment:7 Changed 13 months ago by simonpj

Indeed comment:6 is a separate bug: #16074

Note: See TracTickets for help on using tickets.