$ (apply) is not always a valid substitute for parens

Chat
#1

I’ve gotten into the habit of using $ instead of parenthesis whenever possible, but I sometimes encounter unexpected compilation failures with this approach. Is this a bug, or am I misunderstanding how the type system works?

type Foo = forall a. a -> a
type Bar = forall a. Eq a => a -> a

type Stuff =
  { foo :: Foo
  , bar :: Bar
  }

broken :: Stuff -> Int
broken r =
  r.bar $ r.foo 1

workaround :: Stuff -> Int
workaround r =
  r.bar (r.foo 1)
  
onlyAffectsRecords :: Foo -> Bar -> Int
onlyAffectsRecords foo bar =
  bar $ foo 1

https://try.ps.ai/?gist=da17d1d8086e598ba6a3520aaf2c0517

I don’t know why this issue only occurs when records are involved. It could be similar to this other bug; however, that involves record destructuring, while this example does not.

1 Like
#2

This is due to impredicativity, and there’s quite a bit of literature around this. It’s the same reason you can’t use $ with ST.run. GHC is getting a neat feature in 9.2 called “Quick-Look Impredicativity” if you want to check it out.

The gist of it is that $ is not going to preserve polytypes (foralls, constraints) with our existing type-checker rules. It requires instantiating a type variable with another polytype, which we do not do.

1 Like
#3

Oh, I take that back. I should have read more clearly (gotta stop replying to quickly!). I’m not sure why it wouldn’t work with a record in this case, if it works with individual arguments.

1 Like
#4

My guess would be that there’s a subtle difference in the typechecker between looking up a variable directly in the environment vs inferring the type of record projection.

1 Like
#5

Adding a seemingly-unrelated argument fixes compilation. Still very confused why calling r.baz is okay, but calling r.bar is not.

type Stuff =
  { foo :: forall a. a -> a
  , bar :: forall a. Eq a => a -> a
  , baz :: forall a. Eq a => String -> a -> a
  }

v1 :: Stuff -> Int
v1 r =
  r.baz "thing" $ r.foo 1 -- works if function takes more than one arg
  
v2 :: Stuff -> Int
v2 r =
  r.bar $ r.foo 1 -- fails to compile

https://try.ps.ai/?gist=31b0f70b65ed6d03614b2f1892cd678a

1 Like
#6

For things like that, it might be helpful to walk through the check/infer rules in the compiler to see how they are different, and work out how the compiler is instantiating types. v2 failing to typecheck seems like a very clear bug to me.

2 Likes