Can't unify two equal type literals in some cases

Open
#4,543 0 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

Assessment

Difficulty
5/5
Estimated time
Over a week
Newbie friendliness
35/100
Issue type
Bug
Clarity
Mostly clear
Activity status
Stale
Tech stack
haskell
Domain
compilers

Research direction

Reproduce the four examples with PureScript 0.15.8 and compare the reported type errors. Trace the compiler's handling of row types, magic constraints, and type-literal unification; done means the examples consistently either all typecheck or all fail as specified.

Written by the indexing model from the issue text.

Description

type: bug

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

Dominant language
Haskell
Stars
8.9k
Forks
575
PR merge metrics
No merged PRs in 30d

Contributor guide

Open the contributing guide

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from purescript/purescript

All issues in purescript/purescript

Similar issues

More Haskell issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.