Haskell Rank1Types and parentheses — strange behaviour

Question

Switching on RankNTypes (without which these signatures won't get accepted, because they're not Haskell 98, says the User Guide), and -fprint-explicit-foralls so I can see the quantification, consider:

foo :: b -> (Eq c => c)              -- inferred foo :: forall {c} {b}. Eq c => b -> c
foo x = undefined

bar :: b -> (Eq b => b)              -- inferred bar :: forall {b}. Eq b => b -> b
bar x = undefined

bar2 :: b -> (forall b. Eq b => b)   --          bar2 :: forall {b1} {b}. Eq b1 => b -> b1
bar2 x = undefined

OK so far: these are all Rank 1 Types. GHC (version 8.6.5) has shunted the constraint to the front of the signature; for bar 'commonned' the scope of same-named b; for bar2 not commonned the scope because there's an explicit forall in the given signature, so that's name-shadowing.

barbar :: b -> (Eq b => b) -> (Show b => b)  --  barbar :: forall {b}. Show b => b -> (Eq b => b) -> b
barbar x y = undefined

barbar2 :: b -> Eq b => b -> (Show b => b)   --  barbar2 :: forall {b}. (Eq b, Show b) => b -> b -> b
barbar2 x y = undefined

What's going on with the inferred signature for barbar? That nested -> (Eq b => b) -> is not H98. Does that mean the b is not commonned? No:

*Main> barbar 'c' True
<interactive>:36:12: error:
    * Couldn't match expected type `Char' with actual type `Bool'

So barbar, barbar2 are Rank 1 and have the same effective signature -- or do they?

Addit: (in response to answers)

barbar4 :: b -> (Eq b => b -> (Show b => b)) --  barbar4 :: forall {b}. (Eq b, Show b) => b -> b -> b
barbar4 x y = undefined

barbar, barbar4 are equivalent? So Eq b => in barbar scopes over everything to the right. Then I can see that's Rank-1. Whereas the closing parens nested in the given signature for barbar2 is not merely decoration.

chi chi · Accepted Answer · 2020-08-21T07:25:03

These two types are different. Observe this GHCi session. First, we define your functions. I used Num instead of Eq to better explain what's going on.

> barbar :: b -> (Num b => b) -> (Show b => b) ; barbar _ _ = undefined
> :t barbar
barbar :: forall {b}. Show b => b -> (Num b => b) -> b

> barbar2 :: b -> Num b => b -> (Show b => b) ; barbar2 _ _ = undefined
> :t barbar2
barbar2 :: forall {b}. (Num b, Show b) => b -> b -> b

No surprise, here. Now, we apply both functions choosing b ~ String, which does not satisfy Num. This type checks:

> :t barbar "hello" 5
barbar "hello" 5 :: [Char]

This does not:

> :t barbar2 "hello" 5
    * No instance for (Num [Char]) arising from a use of `barbar2'
    * In the expression: barbar2 "hello" 5

Why? In the first case, it's barbar that has to ensure Num b: the caller can exploit that guarantee to craft the argument. Above, 5 is converted to b (i.e., String) thanks to the provided constraint.

In the second case, it's the caller to barbar2 that has to ensure Num b, so we can not choose b ~ String.

Now, one might wonder how can barbar provide the Num b constraint for a generic b. Indeed, that's impossible since non-numeric types exist. However, we only need to do that if we actually use the second argument in barbar. We don't, so the type checker is satisfied.

Indeed, if we try to use the second argument, we do get an error:

> barbar3 :: b -> (Num b => b) -> (Show b => b) ; barbar3 _ y = y
    * Could not deduce (Num b) arising from a use of `y'

Haskell Rank1Types and parentheses — strange behaviour

2 Answers