Opened 3 years ago
Last modified 20 months ago
#13192 new bug
Ambiguity Caused By PolyKind and Not Helpful Error Messages
Reported by: | Shayan-Najd | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler | Version: | 8.1 |
Keywords: | TypeFamilies | Cc: | simonpj |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | Poor/confusing error message | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | #10789 | Differential Rev(s): | |
Wiki Page: |
Description
The following code results in a confusing/wrong error message, blaming a type variable (a
) being a fixed Skolem variable:
{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE PolyKinds #-} data I a type family F x type instance F (I a) = a identity :: F (I a) -> F (I a) identity x = x
with the error message
• Couldn't match type ‘F (I a0)’ with ‘F (I a)’ Expected type: F (I a) -> F (I a) Actual type: F (I a0) -> F (I a0) NB: ‘F’ is a type function, and may not be injective The type variable ‘a0’ is ambiguous • In the ambiguity check for ‘identity’ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the type signature: identity :: F (I a) -> F (I a) | 9 | identity :: F (I a) -> F (I a) | ^^^^^^^^^^^^^^^^^^
Change History (6)
comment:1 Changed 3 years ago by
comment:2 Changed 3 years ago by
Why does it also not work if I change the definition of F
to
type family F (x :: *) :: k
in which case ghci tells me the instance is
type instance F k (I k a) = a -- Defined at I.hs:7:16
but ghc gives the same error regarding identity
. Is k
not determined by the result kind of the type family, i.e., the fact that F (I a)
appears as a type argument to (->)
?
comment:3 Changed 3 years ago by
Can you explain more precisely why F (I a)
is stuck with PolyKinds
? I don't get it.
comment:4 Changed 3 years ago by
In the original program, the application F (I a)
is stuck because
data I a
really meansdata I k (a :: k) :: *
, i.e.,I
is polykinded
type family F x
really meanstype family F k (x :: *) :: *
, i.e.,F
is not polykinded
type instance F (I a) = a
really meanstype instance F (I * a) = a
, because the instance is only well-kinded whena
has kind*
.
But there's nothing stopping one from adding an additional instance
type instance F (I Maybe) = Char
which usesI
at a different kind.
identity :: F (I a) -> F (I a)
really meansidentity :: forall k (a :: k). F (I k a) -> F (I k a)
, i.e.,identity
is polykinded. Now there's a problem because the instance we defined only applies whenk = *
, but herek
could really be anything, like* -> *
.
And indeed if I added the
type instance F (I Maybe) = Char
, then I can writeidentity @ Maybe
and it has typeChar -> Char
just likeidentity @ Char
does. So the type really is ambiguous.
What I'm confused about is why F (I a)
is still stuck even when I make the result of F
polykinded, so that the instance type instance F (I a) = a
applies at all kinds.
comment:5 Changed 3 years ago by
The type instance in @rwbarton's case expands to F k (I k a) = a
. This instance requires the two k
s to be the same. In identity
's type signature, we get F (TYPE r) (I k a) -> F (TYPE r') (I k a)
. GHC (rightly) doesn't know that k
and TYPE r
are the same. (The fact that it's TYPE r
and not Type
is not the issue.)
comment:6 Changed 20 months ago by
Keywords: | TypeFamilies added |
---|---|
Related Tickets: | → #10789 |
To add more information: this code is accepted without
PolyKinds
, becauseF (I a)
can immediately reduce toa
. WithPolyKinds
,F (I a)
is stuck, as we don't knowa
's kind. (The equation forF
works only when(a :: Type)
.)Perhaps the best fix is to add a check in TcErrors for type families that match on invisible parameters (i.e., kinds) and emit a
NB: Type family `F' has equations that depend on the kind of its argument(s)
.