[ breaking ] remove parsing of dangling binders (#1711)

* [ breaking ] remove parsing of dangling binders

It used to be the case that

```
ID : Type -> Type
ID a = a

test : ID (a : Type) -> a -> a
test = \ a, x => x
```

and

```
head : List $ a -> Maybe a
head [] = Nothing
head (x :: _) = Just x
```

were accepted but these are now rejected because:

* `ID (a : Type) -> a -> a` is parsed as `(ID (a : Type)) -> a -> a`
* `List $ a -> Maybe a` is parsed as `List (a -> Maybe a)`

Similarly if you want to use a lambda / rewrite / let expression as
part of the last argument of an application, the use of `$` or parens
is now mandatory.

This should hopefully allow us to make progress on #1703

Author: gallais

libs/base/Control/Monad/Error/Interface.idr

@@ -94,22 +94,22 @@ public export
 MonadError e m => MonadError e (ReaderT r m) where
   throwError = lift . throwError
   catchError (MkReaderT m) f =
-    MkReaderT \e => catchError (m e) (runReaderT e . f)
+    MkReaderT $ \e => catchError (m e) (runReaderT e . f)
 
 public export
 MonadError e m => MonadError e (StateT r m) where
   throwError = lift . throwError
   catchError (ST m) f =
-    ST \s => catchError (m s) (runStateT s . f)
+    ST $ \s => catchError (m s) (runStateT s . f)
 
 public export
 MonadError e m => MonadError e (RWST r w s m) where
   throwError = lift . throwError
   catchError (MkRWST m) f =
-    MkRWST \r,w,s => catchError (m r w s) (\e => unRWST (f e) r w s)
+    MkRWST $ \r,w,s => catchError (m r w s) (\e => unRWST (f e) r w s)
 
 public export
 MonadError e m => MonadError e (WriterT w m) where
   throwError = lift . throwError
   catchError (MkWriterT m) f =
-    MkWriterT \w => catchError (m w) (\e => unWriterT (f e) w)
+    MkWriterT $ \w => catchError (m w) (\e => unWriterT (f e) w)

libs/base/Control/Monad/RWS/CPS.idr

@@ -43,14 +43,14 @@ execRWST m r s = (\(_,s',w) => (s',w)) <$> runRWST m r s
 public export %inline
 mapRWST : (Functor n, Monoid w, Semigroup w')
         => (m (a, s, w) -> n (b, s, w')) -> RWST r w s m a -> RWST r w' s n b
-mapRWST f m = MkRWST \r,s,w =>
+mapRWST f m = MkRWST $ \r,s,w =>
                 (\(a,s',w') => (a,s',w <+> w')) <$> f (runRWST m r s)
 
 ||| `withRWST f m` executes action `m` with an initial environment
 ||| and state modified by applying `f`.
 public export %inline
 withRWST : (r' -> s -> (r, s)) -> RWST r w s m a -> RWST r' w s m a
-withRWST f m = MkRWST \r,s => uncurry (unRWST m) (f r s)
+withRWST f m = MkRWST $ \r,s => uncurry (unRWST m) (f r s)
 
 --------------------------------------------------------------------------------
 --          RWS Functions
@@ -70,8 +70,8 @@ runRWS m r s = runIdentity (runRWST m r s)
 ||| Construct an RWS computation from a function. (The inverse of `runRWS`.)
 public export %inline
 rws : Semigroup w => (r -> s -> (a, s, w)) -> RWS r w s a
-rws f = MkRWST \r,s,w => let (a, s', w') = f r s
-                          in Id (a, s', w <+> w')
+rws f = MkRWST $ \r,s,w => let (a, s', w') = f r s
+                           in Id (a, s', w <+> w')
 
 ||| Evaluate a computation with the given initial state and environment,
 ||| returning the final value and output, discarding the final state.
@@ -92,7 +92,7 @@ execRWS m r s = let (_,s1,w) = runRWS m r s
 public export %inline
 mapRWS :  (Monoid w, Semigroup w')
        => ((a, s, w) -> (b, s, w')) -> RWS r w s a -> RWS r w' s b
-mapRWS f = mapRWST \(Id p) => Id (f p)
+mapRWS f = mapRWST $ \(Id p) => Id (f p)
 
 ||| `withRWS f m` executes action `m` with an initial environment
 ||| and state modified by applying `f`.
@@ -106,29 +106,29 @@ withRWS = withRWST
 
 public export %inline
 Functor m => Functor (RWST r w s m) where
-  map f m = MkRWST \r,s,w => (\(a,s',w') => (f a,s',w')) <$> unRWST m r s w
+  map f m = MkRWST $ \r,s,w => (\(a,s',w') => (f a,s',w')) <$> unRWST m r s w
 
 public export %inline
 Monad m => Applicative (RWST r w s m) where
-  pure a = MkRWST \_,s,w => pure (a,s,w)
+  pure a = MkRWST $ \_,s,w => pure (a,s,w)
   MkRWST mf <*> MkRWST mx =
-    MkRWST \r,s,w => do (f,s1,w1) <- mf r s w
-                        (a,s2,w2) <- mx r s1 w1
-                        pure (f a,s2,w2)
+    MkRWST $ \r,s,w => do (f,s1,w1) <- mf r s w
+                          (a,s2,w2) <- mx r s1 w1
+                          pure (f a,s2,w2)
 
 public export %inline
 (Monad m, Alternative m) => Alternative (RWST r w s m) where
-  empty = MkRWST \_,_,_ => empty
-  MkRWST m <|> MkRWST n = MkRWST \r,s,w => m r s w <|> n r s w
+  empty = MkRWST $ \_,_,_ => empty
+  MkRWST m <|> MkRWST n = MkRWST $ \r,s,w => m r s w <|> n r s w
 
 public export %inline
 Monad m => Monad (RWST r w s m) where
-  m >>= k = MkRWST \r,s,w => do (a,s1,w1) <- unRWST m r s w
-                                unRWST (k a) r s1 w1
+  m >>= k = MkRWST $ \r,s,w => do (a,s1,w1) <- unRWST m r s w
+                                  unRWST (k a) r s1 w1
 
 public export %inline
 MonadTrans (RWST r w s) where
-  lift m = MkRWST \_,s,w => map (\a => (a,s,w)) m
+  lift m = MkRWST $ \_,s,w => map (\a => (a,s,w)) m
 
 public export %inline
 HasIO m => HasIO (RWST r w s m) where

libs/base/Control/Monad/Reader/Interface.idr

@@ -37,8 +37,8 @@ Monad m => MonadReader stateType (ReaderT stateType m) where
 
 public export %inline
 Monad m => MonadReader r (RWST r w s m) where
-  ask       = MkRWST \r,s,w => pure (r,s,w)
-  local f m = MkRWST \r,s,w => unRWST m (f r) s w
+  ask       = MkRWST $ \r,s,w => pure (r,s,w)
+  local f m = MkRWST $ \r,s,w => unRWST m (f r) s w
 
 public export %inline
 MonadReader r m => MonadReader r (EitherT e m) where
@@ -64,4 +64,4 @@ MonadReader r m => MonadReader r (WriterT w m) where
   -- this should require a Monoid instance to further
   -- accumulate values, while the implementation of
   -- MonadReader for RWST does no such thing.
-  local f (MkWriterT m) = MkWriterT \w => local f (m w)
+  local f (MkWriterT m) = MkWriterT $ \w => local f (m w)

libs/base/Control/Monad/Reader/Reader.idr

@@ -14,7 +14,7 @@ record ReaderT (stateType : Type) (m : Type -> Type) (a : Type) where
 ||| Transform the computation inside a @ReaderT@.
 public export %inline
 mapReaderT : (m a -> n b) -> ReaderT r m a -> ReaderT r n b
-mapReaderT f m = MkReaderT \st => f (runReaderT' m st)
+mapReaderT f m = MkReaderT $ \st => f (runReaderT' m st)
 
 ||| Unwrap and apply a ReaderT monad computation
 public export

libs/base/Control/Monad/State/Interface.idr

@@ -63,9 +63,9 @@ MonadState s m => MonadState s (MaybeT m) where
 
 public export %inline
 Monad m => MonadState s (RWST r w s m) where
-  get     = MkRWST \_,s,w => pure (s,s,w)
-  put s   = MkRWST \_,_,w => pure ((),s,w)
-  state f = MkRWST \_,s,w => let (s',a) = f s in pure (a,s',w)
+  get     = MkRWST $ \_,s,w => pure (s,s,w)
+  put s   = MkRWST $ \_,_,w => pure ((),s,w)
+  state f = MkRWST $ \_,s,w => let (s',a) = f s in pure (a,s',w)
 
 public export %inline
 MonadState s m => MonadState s (ReaderT r m) where

libs/base/Control/Monad/State/State.idr

@@ -61,7 +61,7 @@ execState s = fst . runState s
 ||| the given function.
 public export %inline
 mapState : ((s, a) -> (s, b)) -> State s a -> State s b
-mapState f = mapStateT \(Id p) => Id (f p)
+mapState f = mapStateT $ \(Id p) => Id (f p)
 
 --------------------------------------------------------------------------------
 --          Implementations

libs/base/Control/Monad/Writer/CPS.idr

@@ -44,7 +44,7 @@ execWriterT = map snd . runWriterT
 public export %inline
 mapWriterT :  (Functor n, Monoid w, Semigroup w')
            => (m (a, w) -> n (b, w')) -> WriterT w m a -> WriterT w' n b
-mapWriterT f m = MkWriterT \w =>
+mapWriterT f m = MkWriterT $ \w =>
                   (\(a,w') => (a,w <+> w')) <$> f (runWriterT m)
 
 --------------------------------------------------------------------------------
@@ -72,37 +72,37 @@ execWriter = runIdentity . execWriterT
 public export %inline
 mapWriter :  (Monoid w, Semigroup w')
           => ((a, w) -> (b, w')) -> Writer w a -> Writer w' b
-mapWriter f = mapWriterT \(Id p) => Id (f p)
+mapWriter f = mapWriterT $ \(Id p) => Id (f p)
 
 --------------------------------------------------------------------------------
 --          Implementations
 --------------------------------------------------------------------------------
 
 public export %inline
 Functor m => Functor (WriterT w m) where
-  map f m = MkWriterT \w => (\(a,w') => (f a,w')) <$> unWriterT m w
+  map f m = MkWriterT $ \w => (\(a,w') => (f a,w')) <$> unWriterT m w
 
 public export %inline
 Monad m => Applicative (WriterT w m) where
-  pure a = MkWriterT \w => pure (a,w)
+  pure a = MkWriterT $ \w => pure (a,w)
   MkWriterT mf <*> MkWriterT mx =
-    MkWriterT \w => do (f,w1) <- mf w
-                       (a,w2) <- mx w1
-                       pure (f a,w2)
+    MkWriterT $ \w => do (f,w1) <- mf w
+                         (a,w2) <- mx w1
+                         pure (f a,w2)
 
 public export %inline
 (Monad m, Alternative m) => Alternative (WriterT w m) where
-  empty = MkWriterT \_ => empty
-  MkWriterT m <|> MkWriterT n = MkWriterT \w => m w <|> n w
+  empty = MkWriterT $ \_ => empty
+  MkWriterT m <|> MkWriterT n = MkWriterT $ \w => m w <|> n w
 
 public export %inline
 Monad m => Monad (WriterT w m) where
-  m >>= k = MkWriterT \w => do (a,w1) <- unWriterT m w
-                               unWriterT (k a) w1
+  m >>= k = MkWriterT $ \w => do (a,w1) <- unWriterT m w
+                                 unWriterT (k a) w1
 
 public export %inline
 MonadTrans (WriterT w) where
-  lift m = MkWriterT \w => map (\a => (a,w)) m
+  lift m = MkWriterT $ \w => map (\a => (a,w)) m
 
 public export %inline
 HasIO m => HasIO (WriterT w m) where

libs/base/Control/Monad/Writer/Interface.idr

@@ -60,47 +60,47 @@ public export %inline
 (Monoid w, Monad m) => MonadWriter w (WriterT w m) where
   writer   = writerT . pure
 
-  listen m = MkWriterT \w =>
+  listen m = MkWriterT $ \w =>
                (\(a,w') => ((a,w'),w <+> w')) <$> runWriterT m
 
   tell w'  = writer ((), w')
 
-  pass m   = MkWriterT \w =>
+  pass m   = MkWriterT $ \w =>
                (\((a,f),w') => (a,w <+> f w')) <$> runWriterT m
 
 public export %inline
 (Monoid w, Monad m) => MonadWriter w (RWST r w s m) where
-  writer (a,w') = MkRWST \_,s,w => pure (a,s,w <+> w')
+  writer (a,w') = MkRWST $ \_,s,w => pure (a,s,w <+> w')
 
   tell w' = writer ((), w')
 
-  listen m = MkRWST \r,s,w =>
+  listen m = MkRWST $ \r,s,w =>
                (\(a,s',w') => ((a,w'),s',w <+> w')) <$> runRWST m r s
 
-  pass m = MkRWST \r,s,w =>
+  pass m = MkRWST $ \r,s,w =>
              (\((a,f),s',w') => (a,s',w <+> f w')) <$> runRWST m r s
 
 public export %inline
 MonadWriter w m => MonadWriter w (EitherT e m) where
   writer = lift . writer
   tell   = lift . tell
-  listen = mapEitherT \m => do (e,w) <- listen m
-                               pure $ map (\a => (a,w)) e
+  listen = mapEitherT $ \m => do (e,w) <- listen m
+                                 pure $ map (\a => (a,w)) e
 
-  pass   = mapEitherT \m => pass $ do Right (r,f) <- m
-                                        | Left l => pure $ (Left l, id)
-                                      pure (Right r, f)
+  pass   = mapEitherT $ \m => pass $ do Right (r,f) <- m
+                                          | Left l => pure $ (Left l, id)
+                                        pure (Right r, f)
 
 public export %inline
 MonadWriter w m => MonadWriter w (MaybeT m) where
   writer = lift . writer
   tell   = lift . tell
-  listen = mapMaybeT \m => do (e,w) <- listen m
-                              pure $ map (\a => (a,w)) e
+  listen = mapMaybeT $ \m => do (e,w) <- listen m
+                                pure $ map (\a => (a,w)) e
 
-  pass   = mapMaybeT \m => pass $ do Just (r,f) <- m
-                                       | Nothing => pure $ (Nothing, id)
-                                     pure (Just r, f)
+  pass   = mapMaybeT $ \m => pass $ do Just (r,f) <- m
+                                         | Nothing => pure $ (Nothing, id)
+                                       pure (Just r, f)
 public export %inline
 MonadWriter w m => MonadWriter w (ReaderT r m) where
   writer = lift . writer
@@ -112,8 +112,8 @@ public export %inline
 MonadWriter w m => MonadWriter w (StateT s m) where
   writer = lift . writer
   tell   = lift . tell
-  listen (ST m) = ST \s => do ((s',a),w) <- listen (m s)
-                              pure (s',(a,w))
+  listen (ST m) = ST $ \s => do ((s',a),w) <- listen (m s)
+                                pure (s',(a,w))
 
-  pass   (ST m) = ST \s => pass $ do (s',(a,f)) <- m s
-                                     pure ((s',a),f)
+  pass   (ST m) = ST $ \s => pass $ do (s',(a,f)) <- m s
+                                       pure ((s',a),f)

libs/base/Data/Colist.idr

@@ -215,7 +215,7 @@ inBounds k [] = No uninhabited
 inBounds Z (x::xs) = Yes InFirst
 inBounds (S k) (x::xs) = case inBounds k xs of
   Yes p => Yes $ InLater p
-  No up => No \(InLater p) => up p
+  No up => No $ \(InLater p) => up p
 
 ||| Find a particular element of a Colist using InBounds
 |||

libs/base/Data/Fin/Order.idr

@@ -45,8 +45,8 @@ using (k : Nat)
     connex {y = FZ} _ = Right $ FromNatPrf LTEZero
     connex {x = FS k} {y = FS j} prf =
       case connex {rel = FinLTE} $ prf . (cong FS) of
-        Left  $ FromNatPrf p => Left  $ FromNatPrf $ LTESucc p
-        Right $ FromNatPrf p => Right $ FromNatPrf $ LTESucc p
+        Left  (FromNatPrf p) => Left  $ FromNatPrf $ LTESucc p
+        Right (FromNatPrf p) => Right $ FromNatPrf $ LTESucc p
 
   public export
   Decidable 2 [Fin k, Fin k] FinLTE where