Merge pull request #3401 from buzden/fixity-in-do

[ fix ] Fix ability to declare fixities in `do`

src/Idris/Desugar.idr

@@ -737,10 +737,10 @@ mutual
            pure $ seqFun fc ns tm' rest'
   expandDo side ps topfc ns (DoBind fc nameFC n rig ty tm :: rest)
       = do tm' <- desugarDo side ps ns tm
-           rest' <- expandDo side ps topfc ns rest
            whenJust (isConcreteFC nameFC) $ \nfc => addSemanticDecorations [(nfc, Bound, Just n)]
            ty' <- maybe (pure $ Implicit (virtualiseFC fc) False)
                         (\ty => desugarDo side ps ns ty) ty
+           rest' <- expandDo side ps topfc ns rest
            pure $ bindFun fc ns tm'
                 $ ILam nameFC rig Explicit (Just n) ty' rest'
   expandDo side ps topfc ns (DoBindPat fc pat ty exp alts :: rest)
@@ -749,12 +749,12 @@ mutual
            exp' <- desugarDo side ps ns exp
            alts' <- traverse (map snd . desugarClause ps True) alts
            let ps' = newps ++ ps
-           rest' <- expandDo side ps' topfc ns rest
            let fcOriginal = fc
            let fc = virtualiseFC fc
            let patFC = virtualiseFC (getFC bpat)
            ty' <- maybe (pure $ Implicit fc False)
                         (\ty => desugarDo side ps ns ty) ty
+           rest' <- expandDo side ps' topfc ns rest
            pure $ bindFun fc ns exp'
                 $ ILam EmptyFC top Explicit (Just (MN "_" 0))
                           ty'
@@ -788,12 +788,12 @@ mutual
                        (PatClause fc bpat rest'
                                   :: alts')
   expandDo side ps topfc ns (DoLetLocal fc decls :: rest)
-      = do rest' <- expandDo side ps topfc ns rest
-           decls' <- traverse (desugarDecl ps) decls
+      = do decls' <- traverse (desugarDecl ps) decls
+           rest' <- expandDo side ps topfc ns rest
            pure $ ILocal fc (concat decls') rest'
   expandDo side ps topfc ns (DoRewrite fc rule :: rest)
-      = do rest' <- expandDo side ps topfc ns rest
-           rule' <- desugarDo side ps ns rule
+      = do rule' <- desugarDo side ps ns rule
+           rest' <- expandDo side ps topfc ns rest
            pure $ IRewrite fc rule' rest'
 
   -- Replace all operator by function application

tests/idris2/operators/operators012/Y.idr

@@ -0,0 +1,27 @@
+f : Nat
+f =
+  let (%^%) : Nat -> Nat -> Nat
+      (%^%) = (+)
+      private infixl 1 %^%
+  in 1 %^% 2
+
+g : Nat
+g = do
+  let (%^%%) : Nat -> Nat -> Nat
+      (%^%%) = (+)
+      private infixl 1 %^%%
+  1 %^%% 2
+
+crazy1 : Nat
+crazy1 = do
+  let (%^%%%) : Nat -> Nat -> Nat
+      (%^%%%) = (+)
+  rewrite let private infixl 1 %^%%% in the (Nat = Nat) Refl
+  1 %^%%% 2
+
+crazy2 : List Nat
+crazy2 = do
+  let (%^%%%%) : Nat -> Nat -> Nat
+      (%^%%%%) = (+)
+  x : (let private infixl 1 %^%%%% in Nat) <- [1]
+  pure $ x %^%%%% 2

tests/idris2/operators/operators012/expected

@@ -0,0 +1 @@
+1/1: Building Y (Y.idr)

tests/idris2/operators/operators012/run

@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+check Y.idr