[ treeless ] inline copattern projections in the normalisation pass

src/full/Agda/Compiler/ToTreeless.hs

@@ -118,7 +118,7 @@ casetree cc = do
   case cc of
     CC.Fail -> return C.tUnreachable
     CC.Done xs v -> lambdasUpTo (length xs) $ do
-        v <- lift $ putAllowedReductions [ProjectionReductions, StaticReductions] $ normalise v
+        v <- lift $ putAllowedReductions [ProjectionReductions, CopatternReductions, StaticReductions] $ normalise v
         substTerm v
     CC.Case n (CC.Branches True conBrs _ _) -> lambdasUpTo n $ do
       mkRecord =<< traverse casetree (CC.content <$> conBrs)
@@ -280,22 +280,11 @@ substTerm term = case I.ignoreSharing $ I.unSpine term of
 
 maybeInlineDef :: I.QName -> I.Args -> CC C.TTerm
 maybeInlineDef q vs =
-  ifM (lift $ alwaysInline q) (C.mkTApp <$> inline q <*> substArgs vs) $ do
-  prj <- lift $ isProjection q
-  let noinline = C.mkTApp (C.TDef q) <$> substArgs vs
-  case prj of
-    Just Projection{ projProper = Just _, projIndex = i } | i > 0 ->
-      case vs of
-        v : vs2 | I.Def r es <- unArg v -> do
-          ifM (lift $ not <$> usesCopatterns r) noinline $ do
-            (simp, u) <- lift $ runReduceM $ unfoldDefinition' False (\ v -> return (YesSimplification, pure v))
-                                                               (I.Def r []) r (es ++ [I.Proj q] ++ map I.Apply vs2)
-            case simp of
-              YesSimplification -> substTerm $ I.ignoreBlocking u
-              NoSimplification  -> noinline
-        _ -> noinline
-    _ -> noinline
+  ifM (lift $ alwaysInline q)
+      (C.mkTApp <$> inline q <*> substArgs vs)
+      noinline
   where
+    noinline = C.mkTApp (C.TDef q) <$> substArgs vs
     inline q = lift $ do
       Just cc <- defCompiled <$> getConstInfo q
       casetreeTop cc

src/full/Agda/TypeChecking/Monad/Base.hs

@@ -1381,6 +1381,7 @@ reduced b = case fmap ignoreSharing <$> b of
 data AllowedReduction
   = ProjectionReductions     -- ^ (Projection and) projection-like functions may be reduced.
   | StaticReductions         -- ^ Functions marked STATIC may be reduced.
+  | CopatternReductions      -- ^ Copattern definitions may be reduced.
   | FunctionReductions       -- ^ Functions which are not projections may be reduced.
   | LevelReductions          -- ^ Reduce @'Level'@ terms.
   | NonTerminatingReductions -- ^ Functions that have not passed termination checking.

src/full/Agda/TypeChecking/Reduce.hs

@@ -394,6 +394,10 @@ unfoldDefinition' unfoldDelayed keepGoing v0 f es =
       dontUnfold =
         (defNonterminating info && notElem NonTerminatingReductions allowed)
         || (defDelayed info == Delayed && not unfoldDelayed)
+      copatterns =
+        case def of
+          Function{funCopatternLHS = b} -> b
+          _                             -> False
   case def of
     Constructor{conSrcCon = c} ->
       retSimpl $ notBlocked $ Con (c `withRangeOf` f) [] `applyE` es
@@ -404,7 +408,8 @@ unfoldDefinition' unfoldDelayed keepGoing v0 f es =
     _  -> do
       if FunctionReductions `elem` allowed ||
          (isJust (isProjection_ def) && ProjectionReductions `elem` allowed) || -- includes projection-like
-         (isStaticFun def && StaticReductions `elem` allowed)
+         (isStaticFun def && StaticReductions `elem` allowed) ||
+         (copatterns && CopatternReductions `elem` allowed)
         then
           reduceNormalE keepGoing v0 f (map notReduced es)
                        dontUnfold