Phantom type 'a' is a rigid type variable

Question

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

In qs both elements of the list are of the same type a, while in ps they're of different types P D1 and P D2. The equivalent non-working version of qs would be qs = [ (1 :: Int), (2 :: Double) ] — Fyodor Soikin
But in ps the constraint is being satisfied, so why does the compiler complain? — Lo HaBuyshan
Elements of the list must be all of the same type. Not of different types that all satisfy the same constraint, but of the same type. — Fyodor Soikin
Perhaps you're looking for a list of existentially quantified values, each wrapped up with its own constraint? Then change the type to ps :: [(forall a. C a => P a)], that should work. — Fyodor Soikin
That is what I am looking for apparently. Compiler suggested I use extension RankNTypes, but then complained * Illegal polymorphic type: forall a. C a => P a GHC doesn't yet support impredicative polymorphism * In the type signature: ps :: [(forall a. C a => P a)] — Lo HaBuyshan

chi chi · Accepted Answer · 2021-07-26T23:44:13

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.

Phantom type 'a' is a rigid type variable

2 Answers