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
comment:2 Changed 13 months ago by
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
Related Tickets: | → #13992, #14146 |
---|
comment:4 Changed 13 months ago by
Owner: | set to chessai |
---|---|
Related Tickets: | #13992, #14146 |
I can work on this.
comment:5 Changed 13 months ago by
Related Tickets: | → #13992, #14146 |
---|
(The related tickets were removed for some mysterious reason.)
comment:6 Changed 13 months ago by
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.)
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.