Reputation: 369
{-# LANGUAGE EmptyDataDecls #-}
module Main where
main :: IO ()
main = pure ()
data P a = P Int
data D1
data D2
class C a where
instance C D1 where
instance C D2 where
mkP_D1 :: Int -> P D1
mkP_D1 = P
mkP_D2 :: Int -> P D2
mkP_D2 = P
ps :: C a => [P a]
ps = [mkP_D1 1, mkP_D2 2]
qs :: Num a => [a]
qs = [1, 2]
gives compiler error
Couldn't match type 'a' with 'D1' 'a' is a rigid type variable bound by the type signature for: ps :: forall a. C a => [P a]
Expected type: P a Actual type: P D1
In the expression: mkP_D1 1 In the expression: [mkP_D1 1, mkP_D2 2] In an equation for 'ps': ps = [mkP_D1 1, mkP_D2 2]
Relevant bindings include ps :: [P a]
line 22: ps = [mkP_D1 1, mkP_D2 2]
Why is it that qs
works fine, but yet ps
does not?
Upvotes: 1
Views: 217
Reputation: 116139
I will try to provide some intuition, simplifying things a bit.
ps :: C a => [P a]
is a contract between the implementation of ps
and its user. According to it,
a
C a
holds[P a]
.For instance, the user could choose a ~ D1
. The instance is then used to prove C D1
, so the contract is satisfied. The implementation must then, in this case, provide a value of type [P D1]
.
Your implementation is [mkP_D1 1, mkP_D2 2]
. For the above case, the value mkP_D1 1
follows the contract since it's a P D1
. However, mkP_D2 2
is not a P D1
(but is a P D2
), violating the contract.
Since there is an instance where the user fulfills the contract but the implementation does not, the code is rejected by the type checker.
More pedantically, the issue here is that a
is chosen by the user, not the implementation. If the implementation tries to choose some specific type a
, there is a chance the user will pick something else, and the compiler will rightfully complain in that case.
Why is it that
qs
works fine?
qs :: Num a => [a]
qs = [1, 2]
Here the user chooses a
, but qs
does not. Indeed, 1
is of any (numeric) type a
, and so is 2
.
Compare this with ps
, which tries to choose a
. Incidentally, ps
not only tries to chooses a
to be D1
(which would already trigger the "rigid variable" error), but also tries to choose a
to be D2
(which makes the situation even worse).
A possible working implementation is to add a method to the class:
class C a where
mkP :: Int -> P a
instance C D1 where
mkP = P
instance C D2 where
mkP = P
ps :: C a => [P a]
ps = [mkP 1, mkP 2]
Note that this is only an example. You could use P
directly and avoid introducing the new method in the class.
Upvotes: 3
Reputation: 80724
All elements of a list must have the same type. qs
works because all its elements have the same type a
. ps
doesn't work, because its first element has type P D1
and its second element has type P D2
. Different types. No can do.
From the comments, it became evident that what you're really looking for is for each value to have a different Dx
and pack its own constraint C
with it. To achieve that, wrap it in a GADT:
data PP where
PP :: forall a. C a => P a -> PP
ps :: [PP]
ps = [PP (mkP_D1 1), PP (mkP_D2 2)]
Here, the constructor PP
packs inside of it not only a value P a
, but also the type a
and its corresponding constraint C a
.
Q: Ooooh, but that's so inconvenient! I have to wrap every value in PP
! Can't I do without that?
Short answer - no, you can't. As stated before, all elements of a list must have the same type, period. And if you want to jam different types in there, you have to wrap their differences somehow so they're not visible anymore.
Upvotes: 2