Problem matching apparently similar types in Haskell

Question

This small program works well with concrete types of Int but I wanted to try to make the function the most general with type constraints. The problem is that I don't understand the error message as the two "rigid types" seem to have the same constraints, but can't be matched.

module PotentiationNew where

import Data.Bits (FiniteBits, testBit, finiteBitSize, countLeadingZeros)


potentiation :: (Num a, Integral a, FiniteBits b) => a -> b -> a -> a
potentiation base exponent modulus =
  potentiationGo $ getBits exponent
  where
    potentiationGo :: (Num c, Integral c) => [Bool] -> c
    potentiationGo [] = 1
    potentiationGo (currentExp : restExp)
      | currentExp = (x * x * base) `mod` modulus         -- This is the line with the error
      | otherwise  = (x * x)        `mod` modulus
      where x = potentiationGo restExp
      
    -- Gets a bit array represented as [Bool] (True is 1)
    -- Bit order starts with the least significant bits.
    getBits :: FiniteBits a => a -> [Bool]
    getBits x = testBit x <$> indexed
      where 
        indexed = [0 .. finiteBitSize x - countLeadingZeros x - 1]

Here is the error message:

Potentiation.hs:13:22: error:
    • Couldn't match expected type ‘c’ with actual type ‘a’
      ‘a’ is a rigid type variable bound by
        the type signature for:
          potentiation :: forall a b.
                          (Num a, Integral a, FiniteBits b) =>
                          a -> b -> a -> a
        at Potentiation.hs:6:17
      ‘c’ is a rigid type variable bound by
        the type signature for:
          potentiationGo :: forall c. (Num c, Integral c) => [Bool] -> c
        at Potentiation.hs:10:23

Answer 1

Just because two types have the same constraints doesn't mean they're the same type. For instance, Int is Num, and Integer is Num, but Int is not the same as Integer.

In potentiationGo, you use the values modulus and base, both of which are of type a, in positions where your type signature says there should be a value of type c. These two types aren't the same!

The easiest way to fix your problem is to remove the type signature for potentiationGo, which should remove the error but still keep things general (GHC is pretty good about automatically deriving the most general types).

That said, if you're like me, you really like having the type signature explicit because, at the very least, it acts as a good sanity check and makes your code a little more self-documenting. In this case, what you really want to write is that potentiationGo :: [Bool] -> a, where a is the same a as in your type signature for potentiation itself. If you try this, it won't work, because GHC defaults to creating new type variables for every signature. To counteract this, you need to enable ScopedTypeVariables, which will let GHC know that the two as are the same. This will also mean you need to introduce the type a with the forall keyword (and once you're using forall, you need to introduce every type variable in the type). It'll look something like this:

{-# LANGUAGE ScopedTypeVariables #-}

potentiation :: forall a b. (Num a, Integral a, FiniteBits b) => a -> b -> a -> a
potentiation base exponent modulus =
  potentiationGo $ getBits exponent
  where
    potentiationGo :: [Bool] -> a -- Because the `a` above is in scope and we didn't 
                                  -- write forall here, this a refers to the above one.
    ...

This is as general as you can get.

---

Note that this doesn't affect your getBits function because getBits isn't directly using the value exponent. Rather, that value is being passed as an argument. By this logic, you can also fix potentiationGo by writing something like:

potentiation base' exponent modulus' =
  potentiationGo base' modulus' $ getBits exponent
  where
    potentiationGo :: (Num c, Integral c) => c -> c -> [Bool] -> c
    potentiationGo base modulus [] = 1
    potentiationGo base modulus (currentExp : restExp) = ...

Notice how the values of type a are being provided as arguments to potentiationGo now. Within potentiationGo, the values are of type c. The types c and a are never unified as equal, but because a is Num and Integral, it can be passed to potentiationGo as a c.