Bug in type checker?

1

I’m implementing a type checker in the Lisp macro system and I wanted to do a sanity check by analyzing the same programs in Haskell.

(I’ve enabled RankNTypes and ScopedTypeVariables)

I was confounded by Haskell rejecting this program:

f :: (forall r. r -> r) -> Int
f = g

g :: (String -> String) -> Int
g _ = 1337

I scratched my head for quite a while until I discovered that this program is not rejected:

f :: (forall r. r -> r) -> Int
f x = g x

g :: (String -> String) -> Int
g _ = 1337

Same goes for this. Rejected:

c :: Char
c = f g

f :: ((forall r. r -> r) -> Int) -> Char
f _ = 'x'

g :: (String -> String) -> Int
g _ = 1337

But this is accepted

c :: Char
c = f (\x -> g x)

f :: ((forall r. r -> r) -> Int) -> Char
f _ = 'x'

g :: (String -> String) -> Int
g _ = 1337

I don’t know if it’s a bug technically but it’s still weird. Maybe there’s an underlying problem lurking in the background of the Haskell type checker, waiting to pounce on you.

2 Likes
2

It’s intentional, see the accepted Simplify subsumption proposal.

2 Likes
3

You might enjoy What Haskell’s deep subsumption is, why we killed it, and then why we resurrected it.

6 Likes
4

Interesting.

I’m just smashing parentheses together until they behave but as far as I can tell, I don’t have to worry about “deep subsumption” being a problem. Maybe it will be a problem later. :slight_smile:

Anyway, thank you for the response.

5

Assuming you use GHC, what is the version you used and what exactly is the error message of the rejected programs?
I ask because you are not the first one to fall into this trap, and we could help improve GHCs error messages so that people do not have to ask in forums to understand what is going on.

2 Likes
6

GHC 9.6.7

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

main :: IO ()
main = putStrLn "yo"

c :: Char
c = f g

f :: ((forall r. r -> r) -> Int) -> Char
f _ = 'x'

g :: (String -> String) -> Int
g _ = 1337

Main.hs:8:7: error: [GHC-83865]
    • Couldn't match type: String -> String
                     with: forall r. r -> r
      Expected: (forall r. r -> r) -> Int
        Actual: (String -> String) -> Int
    • In the first argument of ‘f’, namely ‘g’
      In the expression: f g
      In an equation for ‘c’: c = f g
  |
8 | c = f g
7

Sadly, as of today, the error index page does not mention simplified subsumption as the root cause because 83865 is just a general type mismatch.

EDIT: See also related GHC issue and a suggestion.

1 Like
8

Even so, I would support adding it as an example today.

1 Like
9

I’ve made a PR: Add subsumption example to GHC-83865 by noughtmare · Pull Request #562 · haskellfoundation/error-message-index · GitHub

Edit: It’s been merged!

2 Likes
10

Thanks!

You can almost always fix this issue by explicitly applying arguments as shown in the "after" column below.

eta-expansion is the lambda calculus term for that. Would it be more distracting than helpful to mention this name?

11

I thought it wouldn’t really add anything; the intersection of people who’d encounter this error and people who would be much more comfortable with “eta expansion” instead of “explicit function application” seems pretty slim to me.

3 Likes