[ fix #1066 ] do not insert TForce on LHS

When we encounter a delayed (explicit) function type during elaboration
of a LHS, we strip off the delay modality, continue elaboration and return a delayed version of the resulting type.

Note: defining delayed function via pattern matching is not currently
supported. Doing so will require adding a delay marker to LHSs/contexts
familiar from modal type theories. Implicit function are also currently
not supported.

src/Core/Context.idr

@@ -796,6 +796,8 @@ HasNames Error where
   full gam (TTCError x) = pure (TTCError x)
   full gam (FileErr x y) = pure (FileErr x y)
   full gam (CantFindPackage x) = pure (CantFindPackage x)
+  full gam (LazyImplicitFunction fc) = pure (LazyImplicitFunction fc)
+  full gam (LazyPatternVar fc) = pure (LazyPatternVar fc)
   full gam (LitFail fc) = pure (LitFail fc)
   full gam (LexFail fc x) = pure (LexFail fc x)
   full gam (ParseFail xs) = pure (ParseFail xs)
@@ -885,6 +887,8 @@ HasNames Error where
   resolved gam (TTCError x) = pure (TTCError x)
   resolved gam (FileErr x y) = pure (FileErr x y)
   resolved gam (CantFindPackage x) = pure (CantFindPackage x)
+  resolved gam (LazyImplicitFunction fc) = pure (LazyImplicitFunction fc)
+  resolved gam (LazyPatternVar fc) = pure (LazyPatternVar fc)
   resolved gam (LitFail fc) = pure (LitFail fc)
   resolved gam (LexFail fc x) = pure (LexFail fc x)
   resolved gam (ParseFail xs) = pure (ParseFail xs)

src/Core/Core.idr

@@ -161,6 +161,8 @@ data Error : Type where
      TTCError : TTCErrorMsg -> Error
      FileErr : String -> FileError -> Error
      CantFindPackage : String -> Error
+     LazyImplicitFunction : FC -> Error
+     LazyPatternVar :  FC -> Error
      LitFail : FC -> Error
      LexFail : FC -> String -> Error
      ParseFail : List1 (FC, String) -> Error
@@ -346,6 +348,8 @@ Show Error where
   show (TTCError msg) = "Error in TTC file: " ++ show msg
   show (FileErr fname err) = "File error (" ++ fname ++ "): " ++ show err
   show (CantFindPackage fname) = "Can't find package " ++ fname
+  show (LazyImplicitFunction fc) = "Implicit lazy functions are not yet supported"
+  show (LazyPatternVar fc) = "Defining lazy functions via pattern matching is not yet supported"
   show (LitFail fc) = show fc ++ ":Can't parse literate"
   show (LexFail fc err) = show fc ++ ":Lexer error (" ++ show err ++ ")"
   show (ParseFail errs) = "Parse errors (" ++ show errs ++ ")"
@@ -452,6 +456,8 @@ getErrorLoc (GenericMsg loc _) = Just loc
 getErrorLoc (TTCError _) = Nothing
 getErrorLoc (FileErr _ _) = Nothing
 getErrorLoc (CantFindPackage _) = Nothing
+getErrorLoc (LazyImplicitFunction loc) = Just loc
+getErrorLoc (LazyPatternVar loc) = Just loc
 getErrorLoc (LitFail loc) = Just loc
 getErrorLoc (LexFail loc _) = Just loc
 getErrorLoc (ParseFail ((loc, _) ::: _)) = Just loc
@@ -537,6 +543,8 @@ killErrorLoc (GenericMsg fc x) = GenericMsg emptyFC x
 killErrorLoc (TTCError x) = TTCError x
 killErrorLoc (FileErr x y) = FileErr x y
 killErrorLoc (CantFindPackage x) = CantFindPackage x
+killErrorLoc (LazyImplicitFunction fc) = LazyImplicitFunction emptyFC
+killErrorLoc (LazyPatternVar fc) = LazyPatternVar emptyFC
 killErrorLoc (LitFail fc) = LitFail emptyFC
 killErrorLoc (LexFail fc x) = LexFail emptyFC x
 killErrorLoc (ParseFail xs) = ParseFail $ map ((emptyFC,) . snd) $ xs

src/Idris/Error.idr

@@ -614,6 +614,10 @@ perrorRaw (FileErr fname err)
        <++> byShow err
 perrorRaw (CantFindPackage fname)
     = pure $ errorDesc (reflow "Can't find package " <++> pretty0 fname)
+perrorRaw (LazyImplicitFunction fc)
+    = pure $ errorDesc (reflow "Implicit lazy functions are not yet supported.") <+> line <+> !(ploc fc)
+perrorRaw (LazyPatternVar fc)
+    = pure $ errorDesc (reflow "Defining lazy functions via pattern matching is not yet supported.") <+> line <+> !(ploc fc)
 perrorRaw (LitFail fc)
     = pure $ errorDesc (reflow "Can't parse literate.")
         <+> line <+> !(ploc fc)

src/TTImp/Elab/App.idr

@@ -632,9 +632,18 @@ mutual
                         checkExp rig elabinfo env fc tm (glueBack defs env ty) expty
                    else -- Some user defined binding is present while we are out of explicit arguments, that's an error
                         throw (InvalidArgs fc env (map (const (UN $ Basic "<auto>")) autoargs ++ map fst namedargs) tm)
-  -- Function type is delayed, so force the term and continue
-  checkAppWith' rig elabinfo nest env fc tm (NDelayed dfc r ty@(NBind _ _ (Pi _ _ _ _) sc)) argdata expargs autoargs namedargs kr expty
-      = checkAppWith' rig elabinfo nest env fc (TForce dfc r tm) ty argdata expargs autoargs namedargs kr expty
+  -- Function type is delayed:
+  --   RHS: force the term
+  --   LHS: strip off delay but only for explicit functions and disallow any further patterns
+  checkAppWith' rig elabinfo nest env fc tm (NDelayed dfc r ty@(NBind _ _ (Pi _ _ i _) sc)) argdata expargs autoargs namedargs kr expty
+      = if onLHS (elabMode elabinfo)
+           then do when (isImplicit i) $ throw (LazyImplicitFunction fc)
+                   let ([], [], []) = (expargs, autoargs, namedargs)
+                       | _ => throw (LazyPatternVar fc)
+                   (tm, gfty) <- checkAppWith' rig elabinfo nest env fc tm ty argdata expargs autoargs namedargs kr expty
+                   fty <- getTerm gfty
+                   pure (tm, gnf env (TDelayed dfc r fty))
+           else checkAppWith' rig elabinfo nest env fc (TForce dfc r tm) ty argdata expargs autoargs namedargs kr expty
   -- If there's no more arguments given, and the plicities of the type and
   -- the expected type line up, stop
   checkAppWith' rig elabinfo nest env fc tm ty@(NBind tfc x (Pi _ rigb Implicit aty) sc)