Opened 5 years ago

Last modified 12 months ago

#10056 new bug

Inconsistent precedence of ~

Reported by: crockeea Owned by:
Priority: normal Milestone: 8.10.1
Component: Compiler (Parser) Version: 7.8.4
Keywords: Cc: RyanGlScott
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: #10059, #10431, #14316, #15457 Differential Rev(s): Phab:D4876
Wiki Page:

Description

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 (~).

Change History (43)

comment:1 Changed 5 years ago by htebalaka

I was tempted to say precedence rules are the same on the type level (implied by #6027). 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

:/

Last edited 5 years ago by htebalaka (previous) (diff)

comment:2 in reply to:  1 ; Changed 5 years ago by crockeea

Replying to 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.

Last edited 5 years ago by crockeea (previous) (diff)

comment:3 in reply to:  2 Changed 5 years ago by dfeuer

Replying to crockeea:

Replying to 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.

comment:4 Changed 5 years ago by goldfire

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.

comment:5 Changed 5 years ago by goldfire

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

comment:6 Changed 5 years ago by simonpj

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

comment:7 Changed 5 years ago by goldfire

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

comment:8 Changed 4 years ago by goldfire

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

comment:9 Changed 4 years ago by RyanGlScott

Cc: RyanGlScott added

comment:10 Changed 4 years ago by RyanGlScott

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?

comment:11 Changed 4 years ago by simonpj

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

comment:12 Changed 4 years ago by goldfire

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!

comment:13 Changed 4 years ago by RyanGlScott

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.

comment:14 Changed 4 years ago by dfeuer

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.

comment:15 Changed 4 years ago by simonpj

Sounds good to me.

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

comment:16 in reply to:  14 ; Changed 4 years ago by RyanGlScott

Replying to dfeuer:

I would think we'd want it to have even lower precedence than -> to support easy use in contexts.

Is that even possible at the moment? I thought that (->) had the lowest possible precedence:

$ inplace/bin/ghc-stage2 --interactive
GHCi, version 7.11.20150727: http://www.haskell.org/ghc/  :? for help
λ> :i (->)
data (->) a b   -- Defined in ‘GHC.Prim’
infixr 0 `(->)`

comment:17 in reply to:  16 Changed 4 years ago by dfeuer

Replying to RyanGlScott:

Replying to dfeuer:

I would think we'd want it to have even lower precedence than -> to support easy use in contexts.

Is that even possible at the moment? I thought that (->) had the lowest possible precedence:

$ inplace/bin/ghc-stage2 --interactive
GHCi, version 7.11.20150727: http://www.haskell.org/ghc/  :? for help
λ> :i (->)
data (->) a b   -- Defined in ‘GHC.Prim’
infixr 0 `(->)`

Ze who writes the parser makes the rules.

comment:18 Changed 4 years ago by rwbarton

I would expect ~ to have lower precedence than everything except =>. This isn't a totally solid conviction, I could imagine changing my mind if I saw a suitable example, but I can't think of what such an example would look like. If there were built-in type constructors for conjunction/disjunction of constraints, those could have lower precedence than ~, but the only thing we have like that is the tuple syntax, whose parsing doesn't depend on precedence.

By the way, why can't ghci tell me about :i (=>)? :)

Last edited 4 years ago by rwbarton (previous) (diff)

comment:19 Changed 4 years ago by RyanGlScott

How exactly would this work? In order to make (~) have lower precedence than (->), it seems to me we'd have to do one of the following [1]:

  1. Give (~) a negative precedence.
  2. Declare infix 0 ~ and give (->) a higher precedence.

Option 1 sounds particularly scary, since we'd be changing the lower bound of precedences. Option 2 allows users to define their own type operators that have lower precedence than (->), and may cause some existing code to break.

[1] That is, assuming that we're still committed to the idea of non-magically parsing (~) like any other type operator.

comment:20 Changed 4 years ago by rwbarton

I was guessing that your option 1 would in fact be easy, though I haven't looked at any of the code involved.

comment:21 Changed 4 years ago by RyanGlScott

One potential hiccup is that the Haskell 98 Report and the Haskell 2010 Report both require all operators to have an integer precedence from 0 to 9, so we'd have to deviate from those to achieve option 1.

Last edited 4 years ago by RyanGlScott (previous) (diff)

comment:22 in reply to:  21 Changed 4 years ago by dfeuer

Replying to RyanGlScott:

One potential hiccup is that the Haskell 98 Report requires all operators to have an integer precedence from 0 to 9, so we'd have to deviate from that to achieve option 1.

Operator precedence is just syntax. There is no way to write a function f :: OPERATOR -> Int to get the precedence, nor could there be. This just isn't an issue. Allowing users to set arbitrary rational precedence values, or use some sort of general precedence DAG, would require a syntactic extension, but this does not, as it does not allow any new fixity declarations.

comment:23 Changed 4 years ago by RyanGlScott

OK, so the idea is to still require that user-defined fixity declarations have precedence 0–9, but grant exceptions for certain types (e.g., (~)). I think this would technically meet the Haskell 2010 Report, so that's good.

As far as implementation details go, it looks like (->)'s fixity is currently hardwired in BasicTypes.hs, so we could stick in tildeFixity = Fixity (-1) Infix there. I'm not aware of any bounds-checking code that would be tripped up by having a precedence lower than minPrecedence = 0, so I don't think that would be too invasive of a change.

comment:24 Changed 4 years ago by dfeuer

There hasn't been any movement on this in a while, and I'd really like to see it changed. Are there people who disagree with the idea, or is it just a matter of getting it done?

comment:25 Changed 4 years ago by RyanGlScott

I'm not aware of anyone disagreeing, so I don't think that's an obstacle.

I attempted to fix this at one point, but I wasn't experienced enough in GHC to come up with a solution. One huge obstacle (for me, anyway) is that GHC co-opts the tilde symbol for laziness annotations, which means that all occurrences of ~ as type equalities are converted via a special parser function. This makes it much harder to remove ~ as a special parser case, and when I tried removing it, it ended up introducing an enormous number of shift-reduce conflicts.

I would also like to see this fixed at some point, but I don't think I'm going to be the one to fix it.

comment:26 Changed 4 years ago by dfeuer

Oh, I really wasn't talking about removing it as a special case; I was talking about giving it (effectively) a negative precedence. Its current behavior in that regard is very annoying.

comment:27 Changed 4 years ago by goldfire

I few comments as I'm catching up on this thread:

  • We don't need to conform to any standards here. We're talking about type-level operators, so we're already beyond the Haskell reports. Thinking about standards is a Good Thing, but I just want to note that we're already quite off the map.
  • I think that, given the laziness annotation wrinkle, ~ will have to stay somewhat magical in the parser. (That may not have been true when this ticket started, as I think allowing laziness annotations in types came about only with -XStrictData.)
  • However, I think we can eliminate HsEqTy from HsType. Instead, just use HsOpTy with eqTyCon_RDR as the operator. Once we get rid of HsEqTy, I think we'll be well on our way to solving this ticket. Indeed, that's probably a good approach: get rid of HsEqTy and get everything to work again.
  • Parsing -> is magical. And it has to be: we can write forall a. a -> forall b. b -> (a,b), for example. forall can't appear to the right of other operators. And -> has various other special things about it (like being able to appear in record GADT syntax). So we have to keep this in mind.

comment:28 Changed 3 years ago by RyanGlScott

Edward Kmett notes on the ghc-devs mailing list that making -XTypeOperators allow the use of (~) is not a good idea, since it means that other compilers who wish to implement -XTypeOperators must now implement all of the ideas in the OutsideIn(X) paper, which is a big ask. It might be better to introduce a new pragma (-XTypeEqualities?) for this purpose.

comment:29 Changed 3 years ago by RyanGlScott

And as it turns out, -XEqualityConstraints has been proposed before. See #10431.

comment:30 in reply to:  29 Changed 3 years ago by Iceland_jack

never mind

Last edited 3 years ago by Iceland_jack (previous) (diff)

comment:31 Changed 3 years ago by simonpj

I'm all for -XTypeEqualities, if someone wants to specify the details, and implement it.

Simon

comment:32 Changed 2 years ago by RyanGlScott

comment:33 Changed 18 months ago by RyanGlScott

Differential Rev(s): Phab:D4876

Post-d650729f9a0f3b6aa5e6ef2d5fba337f6f70fa60, it's quite easy to remove HsEqTy, at the very least. I've done so in Phab:D4876.

comment:34 Changed 18 months ago by Ben Gamari <ben@…>

In b9483981/ghc:

Remove HsEqTy and XEqTy

After commit d650729f9a0f3b6aa5e6ef2d5fba337f6f70fa60, the
`HsEqTy` constructor of `HsType` is essentially dead code. Given that
we want to remove `HsEqTy` anyway as a part of #10056 (comment:27),
let's just rip it out.

Bumps the haddock submodule.

Test Plan: ./validate

Reviewers: goldfire, bgamari

Reviewed By: bgamari

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #10056

Differential Revision: https://phabricator.haskell.org/D4876

comment:35 Changed 18 months ago by bgamari

Milestone: 8.6.1
Resolution: fixed
Status: newclosed

comment:36 Changed 18 months ago by bgamari

Resolution: fixed
Status: closednew

comment:37 Changed 18 months ago by bgamari

Milestone: 8.6.18.8.1

I believe there is more to do here, but it won't happen for 8.6.

comment:38 Changed 17 months ago by RyanGlScott

An update on this ticket. It seems that the only remaining thing here is to wire in an appropriately low fixity for (~) (and (~~), which GHC introduced after the creation of this ticket). As it turns out, this part is way, way easier than I originally thought. This patch suffices, in fact:

  • compiler/rename/RnFixity.hs

    diff --git a/compiler/rename/RnFixity.hs b/compiler/rename/RnFixity.hs
    index f1bfb38..05d1b89 100644
    a b import Maybes 
    2727import Data.List
    2828import Data.Function    ( on )
    2929import RnUnbound
     30import PrelNames        ( eqTyConKey, heqTyConKey )
     31import Unique
    3032
    3133{-
    3234*********************************************************
    lookupFixityRn_help' name occ 
    124126    --    a>0 `foo` b>0
    125127    -- where 'foo' is not in scope, should not give an error (Trac #7937)
    126128
     129  | name `hasKey` eqTyConKey || name `hasKey` heqTyConKey
     130  = pure (True, Fixity NoSourceText (-2) InfixN)
     131
    127132  | otherwise
    128133  = do { local_fix_env <- getFixityEnv
    129134       ; case lookupNameEnv local_fix_env name of {
  • testsuite/tests/ghci/scripts/T10059.stdout

    diff --git a/testsuite/tests/ghci/scripts/T10059.stdout b/testsuite/tests/ghci/scripts/T10059.stdo
    index 92fbb45..854f52a 100644
    a b  
    11class (a ~ b) => (~) (a :: k0) (b :: k0)       -- Defined in ‘GHC.Types’
     2infix -2 ~
    23(~) :: k0 -> k0 -> Constraint
    34class (a GHC.Prim.~# b) => (~) (a :: k0) (b :: k0)
    45       -- Defined in ‘GHC.Types’
     6infix -2 ~

I'm giving this a precedence of -2, since in #15235, we decided to give (->) a precedence of -1, and the consensus in this ticket is that (~)/(~~) should have a lower precedence than everything else.

Unfortunately, things are never as simple as they appear. Even with this patch, (->) will still have a lower precedence than (~) in practice. Why? Because saying that (->) has a precedence of -1 is a bit of a lie; in reality, it has a precedence closer to -∞, since (->) has special treatment in the parser, which causes it to bind more tightly than it ought to.

Note that (~) is also treated specially in the parser, but there is a post-parsing pass which flattens uses of (~) to appear as ordinary type operators. Perhaps we should extend this treatment to (->) as well?

comment:39 Changed 17 months ago by simonpj

Can someone just summarise why we can't treat (~), from a parsing point of view, as just an ordinary type operator with a specific fixity? With no special treatment in the parser? Why doe we need a "post-parsing pass" for (~)?

And if it's just an ordinary operator, why does it even need to be built-in syntax?

Maybe this all explained above, but a standalone summary would help make sure this ticket is well focused. Thanks!

comment:40 in reply to:  39 Changed 17 months ago by RyanGlScott

When talking about (~), it's important to distinguish between two different uses of it:

  1. As the equality type operator.
  2. As a laziness annotation in -XStrict (e.g., data Foo a = MkFoo ~a).

If it weren't for usage (2), (~) would not need any special treatment at all in the parser. But alas, because of (2), we initially parse all uses of (~) as laziness annotations, and perform an additional pass right after parsing to determine which uses of (~) are for actually for (1), and which are for actually for (2).

(Note that the problems I describe about (->) in comment:38 would still be relevant even if (~) had no special treatment in the parser. In other words, if we decided in the future to have some other type operator with a precedence of -2 or lower, than we'd have to figure out how to answer The (->) Question.)

Once that's taken care of, the fixity of (~) is handled like any other type operator. I only opted to wire in the fixity of (~) in comment:38 since it's negative, and you can't assign a negative fixity through an infix -2 ~ declaration.

comment:41 Changed 17 months ago by simonpj

Ah! I'd forgotten about -XStrict. So the special treatment in Parsery.y is (only) here

strictness :: { Located ([AddAnn], SrcStrictness) }
        : '!' { sL1 $1 ([mj AnnBang $1], SrcStrict) }
        | '~' { sL1 $1 ([mj AnnTilde $1], SrcLazy) }

So is (~) (in types) handled uniformly with (!)? It seems not. Perhaps that's because we don't want to give up (~) as an infix operator, but we are willing to give up (!)?

I got as far as reading splitTilde but got lost in its invocations in RdrHsSyn and Parser.y.

Anyway, it'd be good to summarise how the moving parts fit together, in a Note. There are some e.g. Note [Parsing ~], but they are too brief to do justice to the question.

comment:42 in reply to:  41 Changed 17 months ago by RyanGlScott

Replying to simonpj:

So is (~) (in types) handled uniformly with (!)? It seems not. Perhaps that's because we don't want to give up (~) as an infix operator, but we are willing to give up (!)?

Ugh, that's a very good point. We should be able to use ! as a type operator, but because of this lack of uniformity, we can't. We should fix this.

Anyway, it'd be good to summarise how the moving parts fit together, in a Note. There are some e.g. Note [Parsing ~], but they are too brief to do justice to the question.

Indeed, Note [Parsing ~] could stand to be a bit longer.

I've opened #15457 for both of these issues.

comment:43 Changed 12 months ago by osa1

Milestone: 8.8.18.10.1

Bumping milestones of low-priority tickets.

Note: See TracTickets for help on using tickets.