Add RowLacks

[LiamGoodacre]

I tried to make the error messages a bit nicer, but they are still bad. I wonder if we should just solve it in the compiler instead.

[LiamGoodacre]

Example error:

  29  demo0 = 0 :: RowLacks "k" (k :: String) => Int
              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

  Could not match type

    RowLacking "Existing key found in row" "k"

  with type

    String

  while trying to match type ( k :: RowLacking "Existing key found in row" "k"
                             | t0
                             )
    with type ( k :: String
              , k :: RowLacking "Existing key found in row" "k"
              )
  while solving type class constraint

    Prim.RowCons "k"
                 (RowLacking "Existing key found in row" "k")
                 t0
                 t1

And for the polymorphic case:

  29  demo = 0 :: forall t. RowLacks "k" (k :: t) => Int
             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

  Could not match type

    "Existing key found polymorphically in row"

  with type

    "Existing key found in row"

  while trying to match type RowLacking "Existing key found polymorphically in row"
    with type RowLacking "Existing key found in row"
  while solving type class constraint

    Prim.RowCons "k"
                 (RowLacking "Existing key found polymorphically in row" "k")
                 t0
                 t1

[LiamGoodacre]

I've found another way to do it with a single pass. If I include the row in the RowLacking type then it'll cause an infinite type error in the polymorphic case. The following might be a nicer error?

  28  demo = 0 :: forall t. RowLacks "k" (k :: t) => Int
             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

  An infinite type was inferred for an expression:

    RowLacking "k"
      ( k :: t0
      )

  while trying to match type RowLacking "k"
                               ( k :: t0
                               )
    with type t0
  while solving type class constraint

    Prim.RowCons "k"
                 (RowLacking "k"
                    ( k :: t0
                    )
                 )
                 t1
                 t2

[LiamGoodacre]

Instance chains would be nice here, so we could provide a custom error message 😃

[paf31]

Thanks!

[paf31]

I would actually prefer to simplify RowLacking to something like

data SkolemA
data SkolemB

I know the errors won't be as good, but they're already a little confusing honestly.

You might also be interested in this (older) code from constraints:

http://hackage.haskell.org/package/constraints-0.3.3/docs/src/Data-Constraint-Forall.html#Forall

[LiamGoodacre]

Anything left to do here? :) Let me know if you want something rewording or whatever.

[paf31]

Looks good to me! Sorry for the slow replies.

@garyb Any thoughts here before I merge?

[garyb]

This is pretty fancy! No complaints from me :shipit:

[paf31]

I think this looks good to merge, but before we do, we should consider the alternative of deriving this in the compiler. We're probably going to end up adding a lot of things to work with rows at some point anyway, so it's probably worth considering.

The error messages might be slightly better, for one, but I do like doing things in libraries if possible.

Any thoughts?

[LiamGoodacre]

Just tried this again - I've simplified it, it only uses one skolem type, and the error is a bit better. http://try.purescript.org/?gist=3d4c602fc34075b8a9f99789f903aa80&backend=core&session=40913a4c-d58f-676b-b4ee-cc651d37cff7 Uncomment individual test cases to see the error.

[LiamGoodacre]

Also you never see the Skolem type in the error!

[LiamGoodacre]

Ah, one problem is that I'd have to export RowLacking too 😢. Edit: not a problem, I refactored so that the instance doesn't mention the skolem and if anyone defines other instances they would necessarily overlap.

[paf31]

Very clever! I like it.

[LiamGoodacre]

The errors now look like this:

  16  test = 0 :: RowLacks "k" (k :: Int) => Int
             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

  No type class instance was found for

    Type.Row.RowLacking Entry "k" Int ( k :: Int )

  while checking that type RowLacks "k" ( k :: Int ) => Int
    is at least as general as type Int
  while checking that expression 0
    has type Int
  in value declaration test

And for the polymorphic case:

  16  test = 0 :: forall t. RowLacks "k" (k :: t) => Int
             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

  No type class instance was found for

    Type.Row.RowLacking Entry "k" t0 ( k :: t0 )

  The instance head contains unknown type variables. Consider adding a type annotation.

  while checking that type forall t. RowLacks "k" ( k :: t ) => Int
    is at least as general as type Int
  while checking that expression 0
    has type Int
  in value declaration test

  where t0 is an unknown type

[LiamGoodacre]

I'll squash the commits, then I'm happy with this. Let me know if you want any changes or if you still want to consider solving in the compiler. @paf31 / @garyb

[paf31]

Sorry, could you merge with master? Then I'll merge this and release.

[LiamGoodacre]

@paf31 Rebased :)

[paf31]

Thanks again!