@@ -118,23 +118,20 @@ mkPrec Prefix = Prefix
118118
119119checkConflictingBinding : Ref Ctxt Defs =>
120120 Ref Syn SyntaxInfo =>
121- WithFC OpStr -> (foundFixity : FixityDeclarationInfo ) ->
121+ WithFC OpStr -> (foundFixity : FixityInfo ) ->
122122 (usage : OperatorLHSInfo PTerm) -> (rhs : PTerm) -> Core ()
123123checkConflictingBinding opName foundFixity use_site rhs
124124 = if isCompatible foundFixity use_site
125125 then pure ()
126126 else throw $ OperatorBindingMismatch
127- {print = byShow} opName. fc foundFixity use_site (opNameToEither opName. val) rhs ! candidates
127+ {print = byShow} opName. fc ( DeclaredFixity foundFixity) use_site (opNameToEither opName. val) rhs ! candidates
128128 where
129129
130- isCompatible : FixityDeclarationInfo -> OperatorLHSInfo PTerm -> Bool
131- isCompatible UndeclaredFixity (NoBinder lhs) = True
132- isCompatible UndeclaredFixity _ = False
133- isCompatible (DeclaredFixity fixInfo) (NoBinder lhs) = fixInfo. bindingInfo == NotBinding
134- isCompatible (DeclaredFixity fixInfo) (BindType name ty) = fixInfo. bindingInfo == Typebind
135- isCompatible (DeclaredFixity fixInfo) (BindExpr name expr) = fixInfo. bindingInfo == Autobind
136- isCompatible (DeclaredFixity fixInfo) (BindExplicitType name type expr)
137- = fixInfo. bindingInfo == Autobind
130+ isCompatible : FixityInfo -> OperatorLHSInfo PTerm -> Bool
131+ isCompatible fixInfo (NoBinder lhs) = fixInfo. bindingInfo == NotBinding
132+ isCompatible fixInfo (BindType name ty) = fixInfo. bindingInfo == Typebind
133+ isCompatible fixInfo (BindExpr name expr) = fixInfo. bindingInfo == Autobind
134+ isCompatible fixInfo (BindExplicitType name type expr) = fixInfo. bindingInfo == Autobind
138135
139136 keepCompatibleBinding : BindingModifier -> (Name, GlobalDef) -> Core Bool
140137 keepCompatibleBinding compatibleBinder (name, def) = do
@@ -143,10 +140,7 @@ checkConflictingBinding opName foundFixity use_site rhs
143140 pure compatible
144141
145142 candidates : Core (List String)
146- candidates = do let DeclaredFixity fxInfo = foundFixity
147- | _ => pure [] -- if there is no declared fixity we can't know what's
148- -- supposed to go there.
149- Just (nm, cs) <- getSimilarNames {keepPredicate = Just (keepCompatibleBinding fxInfo. bindingInfo)} opName. val. toName
143+ candidates = do Just (nm, cs) <- getSimilarNames {keepPredicate = Just (keepCompatibleBinding foundFixity. bindingInfo)} opName. val. toName
150144 | Nothing => pure []
151145 ns <- currentNS <$> get Ctxt
152146 pure (showSimilarNames ns opName. val. toName nm cs)
@@ -187,7 +181,7 @@ checkConflictingFixities side usageType opn
187181 -- operator when binding is expected.
188182 whenJust usageType $ \ (l, r) => do
189183 whenJust (head ' $ filter ((/= Prefix ) . fix . snd ) foundFixities) $ \ (_ , fx) =>
190- checkConflictingBinding opn ( DeclaredFixity fx) l r
184+ checkConflictingBinding opn fx l r
191185 throw (GenericMsg opn. fc $ " '\{op}' is not \{opType} operator" )
192186 (fxName, fx) :: _ => do
193187 unless (isCompatible fx ops) $ warnConflict fxName ops
0 commit comments