Purescript treats class as circular type synonym

Question

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?

Answer 1

The error message is misleading and unfortunate - it's not anything you're doing wrong with the code here, it's happening due to how the compiler desugars type classes.

Currently a dictionary is represented as a record, so the synonym mentioned in the error here is because the compiler creates something like this for the class:

type NatClass n = 
  { switch :: forall f. f NatZero -> (forall m. NatClass m => f (NatSucc m)) -> f n }

So that it can do a fairly direct replacement of constraints with dictionary arguments.

I think right now this class (or any that uses itself as a constraint in a member) will have the same problem.

I've been wanting to change the representation for type classes for a while, and have a WIP PR for it, I think after that this kind of thing will be allowed. After this classes will be desugared into a data type rather than a synonym, so the reference should be allowed.

Answer 2

You can work around the Purescript limitation pretty easily by reifying the dictionary yourself. Something like -

data NatZero
data NatSucc n

newtype NatClassDict n = NatClassDict (forall f. f NatZero -> (forall m. NatClass m => f (NatSucc m)) -> f n)

getSwitch :: NatClassDict n -> (forall f. f NatZero -> (forall m. NatClass m => f (NatSucc m)) -> f n)
getSwitch (NatClassDict f) = f

class NatClass n where
  natClassDict :: NatClassDict n

switch :: NatClass n => forall f. f NatZero -> (forall m. NatClass m => f (NatSucc m)) -> f n
switch = getSwitch natClassDict