Pseudo-dependent typing in Haskell

class (Eq k) => MagmaId k where
  type family Zero :: k
  -- data Add  :: k -> k -> k
  -- addIdl :: forall (x :: k) . (Add x Zero :~: x)

instance MagmaId Nat where
  type instance Zero = 0
  -- data Add  = '(+)
  -- addIdl = Refl