Inconsistent precedence of ~

The following compiles as expected:

{-# LANGUAGE TypeFamilies #-}
type family Foo a b

f :: (Foo a b ~ Int) => a -> b -> b
f = error ""

but this fails:

{-# LANGUAGE TypeFamilies #-}
type family a \\ b

f :: (a \\ b ~ Int) => a -> b -> b
f = error ""

with the error

"The second argument of (\\) should have kind *, but b ~ Int has kind Constraint."

Thus the first example is being parsed as (Foo a b) ~ Int, while the second is parsed as a \\ (b ~ Int). I believe the second example should compile, i.e. (\\) and Foo should have the same precedence, both of which are higher than (~).

Trac metadata

Trac field	Value
Version	7.8.4
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Parser)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

mentioned in issue #9194 (closed)

changed weight to 5

added Tbug Trac import parser labels

I was tempted to say precedence rules are the same on the type level (implied by #6027 (closed)). Prefix Foo should have higher precedence then any infix expression, and I thought that infix type operators took the same precedence as their value level versions (though what precedence ~ gets I'm not sure, but I guess it's low), though when I tried to construct a quick example to illustrate in GHCi I didn't get that behaviour:

type family a + b
type instance a + b = a
type family a * b
type instance a * b = b
:kind! Int + Bool * Char
Int + Bool * Char :: *
= Char
:kind! Int + (Bool * Char)
Int + (Bool * Char) :: *
= Int

:/

Replying to [ticket:10056#comment:95804 htebalaka]:

I thought that infix type operators took the same precedence as their value level versions

I'm not sure what you mean by "value level versions". Surely you wouldn't expect the precedence of your type family (+) :: * -> * -> * be related in any way to the function (+) :: (Num a) :: a -> a -> a.

If you mean that the infix precedence is related to the prefix precedence, you are correct: if I set up two type families

type family Foo a b
type family a \\ b
infixr 9 \\

we can ask GHCi

:kind Int \\ Int Foo Int

and it will complain that I can't mix an infixr 9 \\ with infixl 9 Foo``, so this indicates that the infix version of Foo has the same precedence as the prefix version.

Replying to [ticket:10056#comment:95805 crockeea]:

Replying to [ticket:10056#comment:95804 htebalaka]:

I thought that infix type operators took the same precedence as their value level versions

I'm not sure what you mean by "value level versions". Surely you wouldn't expect the precedence of your type family (+) :: * -> * -> * be related in any way to the function (+) :: (Num a) :: a -> a -> a.

I certainly would expect the fixity of the type operator + to be the same as that of the function +, because the parser doesn't know about kinds. It seems the complaint is that ~ has too high a precedence for its purpose.

mentioned in issue #10059 (closed)

Here's what I know about all of this, to the best of my knowledge:

• Types do not "inherit" fixity from terms. The type family (+) :: * -> * -> * (or whatever kinds) is completely and totally unrelated to the term-level variable (+) :: Num a => a -> a -> a.

• There is no way in a fixity declaration to specify what namespace you want the declaration to operate over. So, in (what I consider to be) a terrible hack, a fixity declaration will affect either or both of local term-level and type-level definitions. So, if you have

(//) :: a -> a -> a
(//) = ...
type family (//) a b
infixl 5 //

then both the term (//) and the type (//) get the given fixity. This isn't a case of one inheriting the fixity from the other or being at all related -- it's just a peculiar meaning given to a fixity declaration.

• While the parser doesn't know what type a term has, it does know whether you're writing a term, a type, or a kind. So it can behave differently in each of these cases -- they're all syntactically distinct in Haskell source.

• Traditional fixity declarations don't affect the parser. And, upon some thought, we realize they can't: a fixity declaration can't be acted upon until after (or in) the renamer, when we know where a symbol is declared.

• (~) is parsed separately from the normal infix operators. Recall that TypeOperators used to require type-level operators to begin with :. (~) does not, and so it must be special. Now that TypeOperators has been changed, there actually doesn't seem to be a good reason to keep (~) special. It's declared (in ghc-prim:GHC.Types). It has magic in the solver, but there needs to be no magic dealing with naming or parsing. However, simply removing the magic causes several minor conundrums:

• Do we require TypeOperators when ~ appears in source code? Currently, we don't.
• Do we require TypeFamilies or GADTs when ~ appears in source code? Currently, we do, but if we drop the magic, this decision is suspect, especially if ~ isn't ever really acted on in the module (because it appears only on the RHS of a type synonym, say).
• Should (~) be imported as part of the Prelude? If no, then a lot of code breaks. If yes, that implies that hiding the Prelude also hides (~), breaking less code, but still breaking code.

These issues are surmountable, perhaps, but when I looked at making ~ non-magical, I discovered both that it's technically quite straightforward and socially rather annoying for little benefit. I suppose there's a middle road where it's non-magical in the parser but magical in the renamer.

When I realized how tangled this all was, I gave up, as I was just doing some cleaning. Now that bugs are actually appearing, there might be more incentive to come up with a consistent response.

See also #10059 (closed) for another place where the magic behind (~) causes weird behavior.

Trac metadata

Trac field	Value
Related	→ #10059 (closed)

I would love someone to take this on. It's detail work, but treating (~) more systematically would be a jolly good thing, and a public service.

Simon

See also brief commentary on #9194 (closed), which is a dup of this ticket.

mentioned in issue #10704 (closed)

See also ticket:10704#comment:103034, which points out that :i (~) fails.

What exactly should the precedence of (~) be, anyway? It definitely seems like it should be lower than most things, but how low? For example, should this:

f :: (Int -> Int ~ Int -> Int) => String

parse as this?

f :: ((Int -> Int) ~ (Int -> Int)) => String

Also, I'm not sure that I understand this concern:

Should (~) be imported as part of the Prelude? If no, then a lot of code breaks. If yes, that implies that hiding the Prelude also hides (~), breaking less code, but still breaking code.

Does hiding Prelude necessarily mean that (~) won't be visible? I was under the impression that certain types would still be visible even if Prelude was hidden, e.g., (->). Couldn't we make (~) another such type and sidestep that issue?

As for the LANGUAGE pragma question, I think it would make sense for TypeOperators to enable use of (~). I would keep TypeFamilies and GADTs' ability to enable use of (~) to avoid breaking code unnecessarily—perhaps a warning can be emitted if (~) is used in the presence of TypeFamilies or GADTs but not TypeOperators?

Yes I think we should probably treat (~) as "built-in syntax", like (->) and []. You can't override, import, or hide these things.

Agreed that ~ should be built-in. Using TypeOperators, GADTs or TypeFamilies to enable ~ also makes sense, given the history.

It sounds like you're moving toward the "non-magical in the parser but magical in the renamer" route, which I generally support.

Thanks for pushing this along!

That leaves the remaining question of what fixity to give (~). It seems pretty likely that no matter what is chosen, some code is going to break, so I suppose we should pick a fixity that is as consistent with existing uses of (~) as possible to minimize the fallout.

Currently, it looks like (~) is neither infixl nor infixr, since the following code fails to parse:

f :: (Int ~ Char ~ Bool) => Int; f = 42

I can't think of any scenarios where chaining (~) applications like this would be useful (chime in if you think otherwise!), so that behavior seems alright.

What about the actual precedence? Intuitively, one would imagine (~) to have a very low precedence, as motivated by the original example in this ticket:

{-# LANGUAGE TypeFamilies #-}
type family a \\ b
infixl 9 \\

-- Currently parses like
--
-- a \\ (b ~ Int)
--
-- but probably ought to be
--
-- (a \\ b) ~ Int
f :: (a \\ b ~ Int) => a -> b -> b
f = error ""

If we declared infix 0 ~, that would give the desired behavior. In a couple of corner cases, you'd still have to use parentheses. For example, in order to make Int -> Int ~ Int -> Int parse, you'd need to add parentheses like so: (Int -> Int) ~ (Int -> Int). (Since that example wouldn't have parsed before anyway, this isn't that bad.)

Therefore, it looks like the only existing code that would break from this idea would be ones that abuse (~) parsing magic, as in the aforementioned example. These could easily be fixed by adding parentheses where needed, so this is a very backwards-amenable change.

I would think we'd want it to have even lower precedence than -> to support easy use in contexts. This would require parentheses for some constraint kind applications, but I conjecture that's less common in practice.

Sounds good to me.

Needs examples in the user manual to show what is and is not ok.