a = b does not typecheck despite a and b having the same type and b typechecks

[Renegatto]

Description

Expected, that for any two declarations having the shape either both typecheck or both don't:

a :: A
a = ...

b :: A
b = a

However this bug proves this wrong.

To Reproduce

Consider the function:

succeeds ∷
  ∀ r0.
  Cons "foo" Unit () r0 =>
  Union r0 () r0 =>
  Proxy r0 ->
  Unit
succeeds _ = unsafeThrow ""

This function fails to typecheck:

fails ∷
  ∀ r0.
  Cons "foo" Unit () r0 =>
  Union r0 () r0 =>
  Proxy r0 ->
  Unit
fails = succeeds

Type error

  Could not match type

    ( foo :: Unit
    )

  with type

    r00

Expected behavior

Either both functions typecheck, or both fail.

Additional context

Note, that succeeds constraints can be easily satisfied:

doesntFail ∷ Unit
doesntFail = succeeds (Proxy :: _ (foo :: Unit))

PureScript version

0.15.8

[MonoidMusician]

This is a known issue caused by how PureScript solves Cons constraints with concrete symbols, since it does not have first-class type equalities. See #3243.

I would recommend not using concrete symbols in Cons constraints.