Haskell compiler can't resolve operators exported from Data.Type.Nat module

I attempted to use div operator on natural numbers exported from Data.Type.Nat module,but I got this error:

src\RandomAccessList.hs:54:37: error:
    Not in scope: ‘Data.Nat.div’
    Perhaps you meant one of these:
      data constructor ‘Data.Nat.S’ (imported from Data.Nat),
      data constructor ‘Data.Nat.Z’ (imported from Data.Nat)
    Module ‘Data.Nat’ does not export ‘div’.
   |
54 |                         where m = n Data.Nat.div 2
   |                                     ^^^^^^^^^^^^

Full source code:

module RandomAccessList() where
import Data.Type.Nat
import qualified  Data.Nat


data Tree a = Leaf a | Node Nat (Tree a) (Tree a)

size :: Tree a -> Nat
size (Leaf x) = 1
size (Node n _ _) = n

node ::Tree a -> Tree a -> Tree a
node t1 t2 = Node (size t1 + size t2) t1 t2


data Digit a = Zero | One (Tree a)
type RAList a = [Digit a] --a list of Digit a


fromRA::RAList a -> [a]
{--
[   Zero,
    One (Node 2 (Leaf 'a') (Leaf 'b')),
    One (Node 4 (Node 2 (Leaf 'c') (Leaf 'd'))
                (Node 2 (Leaf 'e') (Leaf 'f')))] 
--}
fromRA = concatMap from
         where  from Zero =[]
                from (One t) = fromT t
fromT ::Tree a -> [a]
fromT (Leaf x) =[x]
fromT (Node _ t1 t2) = fromT t1 ++ fromT t2


fetchRA::Nat -> RAList a -> a
fetchRA k (Zero:xs) = fetchRA k xs
fetchRA k (One t :xs) = if k < size t
                        then fetchT k t else fetchRA (k - size t) xs
fetchT ::Nat -> Tree a -> a
fetchT 0 (Leaf x) = x
fetchT k (Node n t1 t2) = 
                        if k < m
                        then fetchT k t1 else fetchT (k - m) t2
                        where m = n Data.Nat.div 2

If I just use div without any qualifier,I would get this error:

I suppose you are talking about this module: Data.Nat

Firstly, it indeed does not export div. Perhaps you just want div from the Prelude? You can use it unqualified (i.e. no need to prefix with a module name). Secondly, you need to put alphanumeric identifiers in backticks if you use them infix. Does

where m = n `div` 2

do what you want?

1 Like

Your edit convinces me that you do indeed want backticks: where m = n `div` 2.

Adding backticks does solve the problem,thank you.

1 Like