Lo HaBuyshan
Lo HaBuyshan

Reputation: 369

Phantom type 'a' is a rigid type variable

{-# 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

Why is it that qs works fine, but yet ps does not?

Upvotes: 1

Views: 217

Answers (2)

chi
chi

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,

  • the user can choose any a
  • the user must prove that C a holds
  • then, the implementation must provide a value of type [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

Fyodor Soikin
Fyodor Soikin

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

Related Questions