GCD fun

{-# LANGUAGE TypeFamilies, ScopedTypeVariables #-}
module Test where

data Zero
data Succ n

type One = Succ Zero
type Two = Succ One
type Four = Succ (Succ Two)
type Six = Succ (Succ Four)
type Eight = Succ (Succ Six)

class Nat n where
  toInt :: n -> Int

instance Nat Zero where
  toInt _ = 0

instance (Nat n) => Nat (Succ n) where
  toInt _ = 1 + toInt (undefined::n)

type family GCD d m n
type instance GCD d Zero Zero = d
type instance GCD d (Succ m) (Succ n) = GCD (Succ d) m n
type instance GCD Zero (Succ m) Zero = Succ m
type instance GCD (Succ d) (Succ m) Zero = GCD (Succ Zero) d m
type instance GCD Zero Zero (Succ n) = Succ n
type instance GCD (Succ d) Zero (Succ n) = GCD (Succ Zero) d n

fun :: (Nat a, GCD Zero a Four ~ Four) => a -> Int
fun a = toInt a