Inferring a record using Lacks, Union or Cons

Help
#1

Hi. Both, t and tt, fail with the same error: Could not match type r0 with type ( y :: String | t1)

type T r = (x :: Int, y :: String | r)
type T' = T ()

t
  :: forall r
   . Lacks "x" r
  => Union (x :: Int) r T'
  => Record r
t = { y: "s" }

tt
  :: forall r
   . Cons "x" Int r T'
  => Record r
  -> Record r
tt _ = { y: "s" }

What would be a more elaborate reason for why they don’t type check?

#2

A simpler case might be more useful to look at:

t :: forall r. Union () () r => Record r
t = {}

This also doesn’t type check. Even though the constraint Union () () r limits the choice of r to just (), the r has not yet been assigned within the definition of the function and thus Record r is not the same as Record ().

You’d need something like what’s discussed in https://github.com/purescript/purescript/issues/3580 for it to be possible I think

1 Like
#3

You don’t need named functional dependencies, but you do need deferred/implicit type equalities, which the compiler does not support. Type-checking happens before constraint solving, if you want to defer an equality to the constraint solver, you have to opt-in to it explicitly with a TypeEquals constraint and an explicit cast.

2 Likes