Can't unify two equal type literals in some cases

[Renegatto]

Description

It seems that in some cases compiler does not recognize that "(foo" :: Symbol) ~ ("foo" :: Symbol) in presence of row types and their magic constraints.

To Reproduce

Consider the code

class TypeEquals a b | a -> b, b -> a
instance TypeEquals a a


fn :: forall label a r r'. 
  Cons label a r r' =>
  Proxy label ->
  Record r -> 
  Record r'
fn = unsafeThrow "not implemented"

These functions do not typecheck:

1. Cons "foo"; Proxy "foo"
2. Cons foo; Proxy "foo"
3. Cons "foo"; Proxy foo

bothLiterals :: forall a r r'.
  Cons "foo" a r r' =>
  Record r ->
  Record r'
bothLiterals r =
  fn (Proxy :: _ "foo") r -- fails

Type error

  Could not match type

    ( foo :: t1
    | r4
    )

  with type

    r'5

proxyLiteral :: forall a r r' foo.
  TypeEquals foo "foo" =>
  Cons foo a r r' =>
  Record r ->
  Record r'
proxyLiteral r =
  fn (Proxy :: _ "foo") r -- fails

Type error

  Could not match type

    ( foo :: t1
    | r4
    )

  with type

    r'5

consLiteral :: forall a r r' foo.
  TypeEquals foo "foo" =>
  Cons "foo" a r r' =>
  Record r ->
  Record r'
consLiteral r = fn (Proxy :: _ foo) r -- fails

Type error

  No type class instance was found for

    Prim.Row.Cons foo4
                  t1
                  r5
                  r'6

And this one typechecks:

• Cons foo; Proxy foo

onlyTyVars :: forall a r r' foo.
  TypeEquals foo "foo" =>
  Cons foo a r r' =>
  Record r ->
  Record r'
onlyTyVars r = fn (Proxy :: _ foo) r

Expected behavior

Either all the examples cases typecheck well, or none of them do.

Additional context

Note, that if any of the functions was implemented, it would work well with foo ~ "foo". For instance this typechecks well:

f :: forall a r.
  Record r ->
  Record (foo :: a | r)
f = consLiteral -- using one of the functions that didn't typecheck

PureScript version

0.15.8