title: Haskell - How to define the dependent type Remainder (i.e. Rmndr modulo)?
body: <p>My understanding is that the remainder type is a dependent type (depending on the modulo). I read about the DataKinds extension and was able to define it like the following:</p>
  
  <pre><code>{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators, GADTs #-}
  data Nat = Zero | Succ Nat
  
  data Rmndr modulo where
      Nil :: Rmndr Zero
      Rmndr :: Integer -&gt; Rmndr modulo
  </code></pre>
  
  <p>But then when I preceeded to implement the Eq class, I stuck at the condition</p>
  
  <pre><code>Rmndr x == Rmndr y = (x `mod` modulo) == (y `mod` modulo)
  </code></pre>
  
  <p>because modulo is not a value, but a type. Even if we can write a function as follow:</p>
  
  <pre><code>decat :: Nat -&gt; Integer
  decat Zero = 0
  decat (Succ nat) = decat nat + 1
  </code></pre>
  
  <p>we cannot use it as follows</p>
  
  <pre><code>instance Eq (Rmndr modulo) where
      Nil == Nil = True
      Rmndr x == Rmndr y =
          x `mod` (decat modulo) == y `mod` (decat modulo)
  </code></pre>
  
  <p>because "modulo" in this syntax is not a variable.</p>
  
  <p>Can any one help on this puzzle? Thanks a lot! </p>