Confused about how PureScript checks RowList's instances

Sorry if the title is misleading, I wasn’t sure how to phrase it properly.

My issue is pretty simple, I’d like to have a Record type, where all the fields are “Encodable” (implement Encode from Foreign.Generic). In order to do so, I wrote some simple classes and instances:

class Encodable (row :: #Type)

instance encodable ::
  ( RowToList row list
  , EncodableRowList list
  ) =>
  Encodable row

class EncodableRowList (rowList :: RowList)

instance encodableRowListCons ::
  ( EncodableRowList tail
  , Encode fieldType
  ) =>
  EncodableRowList (Cons symbol fieldType tail)

instance encodableRowListNil :: EncodableRowList Nil

When testing the above type, I was pretty surprised to see that the following compiles:

data NotEncodable
  = NotEncodable

eRecord :: Encodable ( foo :: NotEncodable ) => Record ( foo :: NotEncodable )
eRecord = { foo: NotEncodable }

But, the following doesn’t compile (which is the desired behavior):

f :: forall r. Encodable r => Record r -> String
f _ = "foo"

x :: String
x = f { foo: NotEncodable }
No type class instance was found for

    Foreign.Generic.Class.Encode NotEncodable

Trying with an “encodable” type does compile as expected:

x :: String
x = f { foo: "foo" }

I’m a bit puzzled here :confused:

This isn’t anything to do with RowList in particular, this is a matter of how type class constraints work in general. When you write this:

eRecord :: Encodable ( foo :: NotEncodable ) => Record ( foo :: NotEncodable )
eRecord = { foo: NotEncodable }

what you’re saying is that at the use site of eRecord, there needs to be an instance Encodable ( foo :: NotEncodable ) in scope. Simply defining the value as you’ve done here does not assert that such an instance exists. What you’ve done is that you’ve written a ‘function’ which is impossible to ‘call’, because the caller isn’t going to be able to provide the required Encodable instance.

If you want to verify that there is no instance for Encodable ( foo :: NotEncodable ), then you can try to discharge the constraint, by writing something like this:

eRecord :: { foo :: NotEncodable }

at which point I think you will see the error you are expecting.

I think this is a case where it’s helpful to consider the way type classes are desugared. In this case, the type class Encodable doesn’t have any members so it gets desugared to something along the lines of:

data Encodable (row :: # Type) = Encodable

and then your eRecord becomes

eRecord :: Encodable (foo :: NotEncodable) -> Record (foo :: NotEncodable)

which is a perfectly acceptable type for a function to have, even if you can’t ever get hold of a value whose type is Encodable (foo :: NotEncodable). It’s similar to how absurd :: forall a. Void -> a is a perfectly acceptable function, even though you can never call it.