@@ -158,9 +158,10 @@ checkConflictingBinding opName foundFixity use_site rhs
158158-- Once conflicts are handled we return the operator precedence we found.
159159checkConflictingFixities : {auto s : Ref Syn SyntaxInfo} ->
160160 {auto c : Ref Ctxt Defs} ->
161- (usageType : Maybe BindingModifier) -> -- `Nothing` for prefix
161+ (side : Side) ->
162+ (usageType : Maybe (OperatorLHSInfo PTerm, PTerm)) -> -- `Nothing` for prefix
162163 WithFC (OpStr' Name ) -> Core (OpPrec , FixityDeclarationInfo )
163- checkConflictingFixities usageType opn
164+ checkConflictingFixities side usageType opn
164165 = do let op = nameRoot opn. val. toName
165166 foundFixities@(_ :: _ ) <- getFixityInfo op
166167 | [] => do
@@ -172,13 +173,25 @@ checkConflictingFixities usageType opn
172173 Backticked _ => pure (NonAssoc 1 , UndeclaredFixity ) -- Backticks are non associative by default
173174
174175 let (opType, f) : (String , _ ) = case usageType of
175- Nothing => (" a prefix" , (== Prefix ) . fix)
176- Just b => (" a \{show b} infix" , \ op => op. fix /= Prefix && op. bindingInfo == b)
176+ Nothing => (" a prefix" , (== Prefix ) . fix)
177+ Just (b, _ ) => do
178+ let b = b. getBinder
179+ (" a \{show b} infix" , \ op => op. fix /= Prefix && (op. bindingInfo == b || side == LHS ))
177180 let ops = filter (f . snd ) foundFixities
178181
179- let (fxName, fx) :: _ = ops | [] => throw (GenericMsg opn. fc $ " '\{op}' is not \{opType} operator" )
180- unless (isCompatible fx ops) $ warnConflict fxName ops
181- pure (mkPrec fx. fix fx. precedence, DeclaredFixity fx)
182+ case ops of
183+ [] => do
184+ unless (side == LHS ) $ -- do not check for conflicting fixity on the LHS
185+ -- This is because we do not parse binders on the lhs
186+ -- and so, if we check, we will find uses of regular
187+ -- operator when binding is expected.
188+ whenJust usageType $ \ (l, r) => do
189+ whenJust (head ' $ filter ((/= Prefix ) . fix . snd ) foundFixities) $ \ (_ , fx) =>
190+ checkConflictingBinding opn (DeclaredFixity fx) l r
191+ throw (GenericMsg opn. fc $ " '\{op}' is not \{opType} operator" )
192+ (fxName, fx) :: _ => do
193+ unless (isCompatible fx ops) $ warnConflict fxName ops
194+ pure (mkPrec fx. fix fx. precedence, DeclaredFixity fx)
182195 where
183196 -- Fixities are compatible with all others of the same name that share the same
184197 -- fixity, precedence, and binding information
@@ -222,16 +235,11 @@ parameters (side : Side)
222235 {auto c : Ref Ctxt Defs} ->
223236 PTerm -> Core (List (Tok ((OpStr, FixityDeclarationInfo), Maybe (OperatorLHSInfo PTerm)) PTerm))
224237 toTokList (POp fc (MkWithData _ l) opn r)
225- = do (precInfo, fixInfo) <- checkConflictingFixities (Just l. getBinder) opn
226- unless (side == LHS ) -- do not check for conflicting fixity on the LHS
227- -- This is because we do not parse binders on the lhs
228- -- and so, if we check, we will find uses of regular
229- -- operator when binding is expected.
230- (checkConflictingBinding opn fixInfo l r)
238+ = do (precInfo, fixInfo) <- checkConflictingFixities side (Just (l, r)) opn
231239 rtoks <- toTokList r
232240 pure (Expr l. getLhs :: Op fc opn. fc ((opn. val, fixInfo), Just l) precInfo :: rtoks)
233241 toTokList (PPrefixOp fc opn arg)
234- = do (precInfo, fixInfo) <- checkConflictingFixities Nothing opn
242+ = do (precInfo, fixInfo) <- checkConflictingFixities side Nothing opn
235243 rtoks <- toTokList arg
236244 pure (Op fc opn. fc ((opn. val, fixInfo), Nothing ) precInfo :: rtoks)
237245 toTokList t = pure [Expr t]
0 commit comments