I'm trying to define instances that only work on type level natural numbers. When I compile this file:
module Main where
data NatZero
data NatSucc n
class NatClass n where
switch :: f NatZero -> (forall m. NatClass m => f (NatSucc m)) -> f n
it tells me:
Error found:
at src/Main.purs:6:1 - 7:73 (line 6, column 1 - line 7, column 73)
A cycle appears in the definition of type synonym NatClass
Cycles are disallowed because they can lead to loops in the type checker.
Consider using a 'newtype' instead.
Why did NatClass become a type synonym? I thought it was a type class. And where is there a loop? What should I change to make this work like in Haskell? It's telling me to newtype, what do I newtype?