Fix #5809: retain parameters for irrelevant projections.

Since irrelevant projections are not reduced since Agda 2.6.1,
they can lead to non-inferable terms if they drop their parameters.

A simple solution (implemented here) is to retain parameters for all
irrelevant projection, treating them as ordinary functions on the rhs.

src/full/Agda/Compiler/ToTreeless.hs

@@ -486,6 +486,7 @@ mkRecord fs = lift $ do
 recConFromProj :: QName -> TCM I.ConHead
 recConFromProj q = do
   caseMaybeM (isProjection q) __IMPOSSIBLE__ $ \ proj -> do
+    -- Get the record type name @d@ from the projection.
     let d = unArg $ projFromType proj
     getRecordConstructor d
 

src/full/Agda/Termination/RecCheck.hs

@@ -58,7 +58,7 @@ recursive names = do
   let nonRec = mapMaybe (\case{ AcyclicSCC x -> Just x ; _ -> Nothing}) sccs
   let recs   = mapMaybe (\case{ CyclicSCC xs -> Just xs; _ -> Nothing}) sccs
 
-  reportSLn "rec.graph" 20 $ show graph
+  reportSLn "rec.graph" 60 $ show graph
 
   -- Mark all non-recursive functions and their clauses as such.
   mapM_ markNonRecursive nonRec

src/full/Agda/TypeChecking/CheckInternal.hs

@@ -346,8 +346,8 @@ inferDef f es = do
 -- | Infer possibly projection-like function application
 inferDef' :: (MonadCheckInternal m) => QName -> Arg Term -> Elims -> m Type
 inferDef' f a es = do
-  isProj <- isProjection f
-  case isProj of
+  -- Andreas, 2022-03-07, issue #5809: don't drop parameters of irrelevant projections.
+  isRelevantProjection f >>= \case
     Just Projection{ projIndex = n } | n > 0 -> do
       let self = unArg a
       b <- infer self

src/full/Agda/TypeChecking/Conversion.hs

@@ -197,8 +197,10 @@ compareAs cmp a u v = do
         (Def f es, Def f' es') | f == f' ->
           ifNotM (optFirstOrder <$> pragmaOptions) fallback $ {- else -} unlessSubtyping $ do
           def <- getConstInfo f
-          -- We do not shortcut projection-likes
-          if isJust $ isProjection_ (theDef def) then fallback else do
+          -- We do not shortcut projection-likes,
+          -- Andreas, 2022-03-07, issue #5809:
+          -- but irrelevant projections since they are applied to their parameters.
+          if isJust $ isRelevantProjection_ def then fallback else do
           pol <- getPolarity' cmp f
           compareElims pol [] (defType def) (Def f []) es es' `orelse` fallback
         _               -> fallback
@@ -397,8 +399,8 @@ computeElimHeadType f es es' = do
   def <- getConstInfo f
   -- To compute the type @a@ of a projection-like @f@,
   -- we have to infer the type of its first argument.
-  if projectionArgs (theDef def) <= 0 then return $ defType def else do
-    -- Find an first argument to @f@.
+  if projectionArgs def <= 0 then return $ defType def else do
+    -- Find a first argument to @f@.
     let arg = case (es, es') of
               (Apply arg : _, _) -> arg
               (_, Apply arg : _) -> arg

src/full/Agda/TypeChecking/InstanceArguments.hs

@@ -601,7 +601,8 @@ applyDroppingParameters t vs = do
         Constructor {conPars = n} -> return $ Con c ci (map Apply $ drop n vs)
         _ -> __IMPOSSIBLE__
     Def f [] -> do
-      mp <- isProjection f
+      -- Andreas, 2022-03-07, issue #5809: don't drop parameters of irrelevant projections.
+      mp <- isRelevantProjection f
       case mp of
         Just Projection{projIndex = n} -> do
           case drop n vs of

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

@@ -266,8 +266,8 @@ lookupSection m = maybe EmptyTel (^. secTelescope) <$> getSection m
 addDisplayForms :: QName -> TCM ()
 addDisplayForms x = do
   reportSDoc "tc.display.section" 20 $ "Computing display forms for" <+> pretty x
-  def <- theDef <$> getConstInfo x
-  let v = case def of
+  def <- getConstInfo x
+  let v = case theDef def of
              Constructor{conSrcCon = h} -> Con h{ conName = x } ConOSystem []
              _                          -> Def x []
 
@@ -1225,7 +1225,7 @@ droppedPars d = case theDef d of
     Axiom{}                  -> 0
     DataOrRecSig{}           -> 0
     GeneralizableVar{}       -> 0
-    def@Function{}           -> projectionArgs def
+    def@Function{}           -> projectionArgs d
     Datatype  {dataPars = _} -> 0  -- not dropped
     Record     {recPars = _} -> 0  -- not dropped
     Constructor{conPars = n} -> n
@@ -1244,6 +1244,15 @@ isProjection_ def =
     Function { funProjection = result } -> result
     _                                   -> Nothing
 
+-- | Is it the name of a non-irrelevant record projection?
+{-# SPECIALIZE isProjection :: QName -> TCM (Maybe Projection) #-}
+isRelevantProjection :: HasConstInfo m => QName -> m (Maybe Projection)
+isRelevantProjection qn = isRelevantProjection_ <$> getConstInfo qn
+
+isRelevantProjection_ :: Definition -> Maybe Projection
+isRelevantProjection_ def =
+  if isIrrelevant def then Nothing else isProjection_ $ theDef def
+
 -- | Is it a function marked STATIC?
 isStaticFun :: Defn -> Bool
 isStaticFun = (^. funStatic)
@@ -1260,20 +1269,21 @@ isProperProjection d = caseMaybe (isProjection_ d) False $ \ isP ->
   (projIndex isP > 0) && isJust (projProper isP)
 
 -- | Number of dropped initial arguments of a projection(-like) function.
-projectionArgs :: Defn -> Int
-projectionArgs = maybe 0 (max 0 . pred . projIndex) . isProjection_
+projectionArgs :: Definition -> Int
+projectionArgs = maybe 0 (max 0 . pred . projIndex) . isRelevantProjection_
 
 -- | Check whether a definition uses copatterns.
 usesCopatterns :: (HasConstInfo m) => QName -> m Bool
 usesCopatterns q = defCopatternLHS <$> getConstInfo q
 
 -- | Apply a function @f@ to its first argument, producing the proper
---   postfix projection if @f@ is a projection.
+--   postfix projection if @f@ is a projection which is not irrelevant.
 applyDef :: (HasConstInfo m)
          => ProjOrigin -> QName -> Arg Term -> m Term
 applyDef o f a = do
   let fallback = return $ Def f [Apply a]
-  caseMaybeM (isProjection f) fallback $ \ isP -> do
+  -- Andreas, 2022-03-07, issue #5809: don't drop parameters of irrelevant projections.
+  caseMaybeM (isRelevantProjection f) fallback $ \ isP -> do
     if projIndex isP <= 0 then fallback else do
       -- Get the original projection, if existing.
       if isNothing (projProper isP) then fallback else do

src/full/Agda/TypeChecking/Positivity.hs

@@ -263,10 +263,7 @@ checkStrictlyPositive mi qset = do
 
 getDefArity :: Definition -> TCM Int
 getDefArity def = do
-  let dropped = case theDef def of
-        defn@Function{} -> projectionArgs defn
-        _ -> 0
-  subtract dropped <$> arity' (defType def)
+  subtract (projectionArgs def) <$> arity' (defType def)
   where
   -- A variant of "\t -> arity <$> instantiateFull t".
   arity' :: Type -> TCM Int

src/full/Agda/TypeChecking/ProjectionLike.hs

@@ -87,7 +87,7 @@ import Agda.Utils.Size
 
 import Agda.Utils.Impossible
 
--- | View for a @Def f (Apply a : es)@ where @isProjection f@.
+-- | View for a @Def f (Apply a : es)@ where @isRelevantProjection f@.
 --   Used for projection-like @f@s.
 data ProjectionView
   = ProjectionView
@@ -117,7 +117,7 @@ projView :: HasConstInfo m => Term -> m ProjectionView
 projView v = do
   let fallback = return $ NoProjection v
   case v of
-    Def f es -> caseMaybeM (isProjection f) fallback $ \ isP -> do
+    Def f es -> caseMaybeM (isRelevantProjection f) fallback $ \ isP -> do
       if projIndex isP <= 0 then fallback else do
         case es of
           []           -> return $ LoneProjectionLike f $ projArgInfo isP
@@ -226,6 +226,8 @@ eligibleForProjectionLike d = eligible . theDef <$> getConstInfo d
 --         Thus, an application of @f@ waiting for a projection
 --         can be stuck even when the principal argument is a constructor.
 --
+--      g. @f@ cannot be an irrelevant definition (Andreas, 2022-03-07, #5809),
+--         as those are not reduced.
 --
 -- For internal reasons:
 --
@@ -247,7 +249,9 @@ makeProjection x = whenM (optProjectionLike <$> pragmaOptions) $ do
     [ "Checking for projection likeness "
     , prettyTCM x <+> " : " <+> prettyTCM t
     ]
-  case theDef defn of
+  if isIrrelevant defn then
+    reportSDoc "tc.proj.like" 30 $ "  projection-like functions cannot be irrelevant"
+  else case theDef defn of
     Function{funClauses = cls}
       | any (isNothing . clauseBody) cls ->
         reportSLn "tc.proj.like" 30 $ "  projection-like functions cannot have absurd clauses"

src/full/Agda/TypeChecking/ReconstructParameters.hs

@@ -24,6 +24,7 @@ import Agda.TypeChecking.Datatypes
 
 import Agda.Utils.Size
 import Agda.Utils.Either
+import Agda.Utils.Function (applyWhen)
 
 import Agda.Utils.Impossible
 
@@ -172,23 +173,18 @@ reconstructParameters' act a v = do
     applyWithoutReversing _            _   = __IMPOSSIBLE__
 
     mapHide (El _ (Pi a b)) (p:tl) =
-      case argInfoHiding (domInfo a) of
-        Hidden -> (hideAndRelParams p):(mapHide (unAbs b) tl)
-        _      -> p:(mapHide (unAbs b) tl)
+      applyWhen (getHiding a == Hidden) hideAndRelParams p : mapHide (unAbs b) tl
     mapHide t l = l
 
 dropParameters :: TermLike a => a -> TCM a
-dropParameters = traverseTermM dropPars
-  where
-    dropPars v =
-      case v of
+dropParameters = traverseTermM $
+    \case
         Con c ci vs -> do
           Constructor{ conData = d } <- theDef <$> getConstInfo (conName c)
           Just n <- defParameters <$> getConstInfo d
           return $ Con c ci $ drop n vs
-        Def f vs -> do
-          isProj <- isProjection f
-          case isProj of
+        v@(Def f vs) -> do
+          isRelevantProjection f >>= \case
             Nothing -> return v
             Just pr -> return $ applyE (projDropPars pr ProjSystem) vs
-        _        -> return v
+        v -> return v

src/full/Agda/TypeChecking/Reduce.hs

@@ -598,12 +598,14 @@ unfoldDefinitionStep unfoldDelayed v0 f es =
       -- (i.e., those that failed the termination check)
       -- and delayed definitions
       -- are not unfolded unless explicitly permitted.
-      dontUnfold =
-        (defNonterminating info && SmallSet.notMember NonTerminatingReductions allowed)
-        || (defTerminationUnconfirmed info && SmallSet.notMember UnconfirmedReductions allowed)
-        || (defDelayed info == Delayed && not unfoldDelayed)
-        || prp == Right True || isIrrelevant (defArgInfo info)
-        || not defOk
+      dontUnfold = or
+        [ defNonterminating info && SmallSet.notMember NonTerminatingReductions allowed
+        , defTerminationUnconfirmed info && SmallSet.notMember UnconfirmedReductions allowed
+        , defDelayed info == Delayed && not unfoldDelayed
+        , prp == Right True
+        , isIrrelevant info
+        , not defOk
+        ]
       copatterns = defCopatternLHS info
   case def of
     Constructor{conSrcCon = c} -> do
@@ -616,12 +618,20 @@ unfoldDefinitionStep unfoldDelayed v0 f es =
                              cls (defCompiled info) rewr
         else noReduction $ notBlocked v
     PrimitiveSort{ primSort = s } -> yesReduction NoSimplification $ Sort s `applyE` es
+
     _  -> do
-      if (RecursiveReductions `SmallSet.member` allowed) ||
-         (isJust (isProjection_ def) && ProjectionReductions `SmallSet.member` allowed) || -- includes projection-like
-         (isInlineFun def && InlineReductions `SmallSet.member` allowed) ||
-         (definitelyNonRecursive_ def && copatterns && CopatternReductions `SmallSet.member` allowed) ||
-         (definitelyNonRecursive_ def && FunctionReductions `SmallSet.member` allowed)
+      if or
+          [ RecursiveReductions `SmallSet.member` allowed
+          , isJust (isProjection_ def) && ProjectionReductions `SmallSet.member` allowed
+              -- Includes projection-like and irrelevant projections.
+              -- Note: irrelevant projections lead to @dontUnfold@ and
+              -- so are not actually unfolded.
+          , isInlineFun def && InlineReductions `SmallSet.member` allowed
+          , definitelyNonRecursive_ def && or
+            [ copatterns && CopatternReductions `SmallSet.member` allowed
+            , FunctionReductions `SmallSet.member` allowed
+            ]
+          ]
         then
           reduceNormalE v0 f (map notReduced es) dontUnfold
                        (defClauses info) (defCompiled info) rewr

src/full/Agda/TypeChecking/Rules/Application.hs

@@ -263,7 +263,8 @@ inferApplication exh hd args e = postponeInstanceConstraints $ do
 
 inferHeadDef :: ProjOrigin -> QName -> TCM (Elims -> Term, Type)
 inferHeadDef o x = do
-  proj <- isProjection x
+  -- Andreas, 2022-03-07, issue #5809: don't drop parameters of irrelevant projections.
+  proj <- isRelevantProjection x
   rel  <- getRelevance . defArgInfo <$> getConstInfo x
   let app =
         case proj of

test/Succeed/Issue5809.agda

@@ -0,0 +1,32 @@
+-- Andreas, 2022-03-07, issue #5809 reported by jamestmartin
+-- Regression in Agda 2.6.1.
+-- Not reducing irrelevant projections lead to non-inferable elim-terms
+-- and consequently to internal errors.
+--
+-- The fix is to treat irrelevant projections as just functions,
+-- retaining their parameters, so that they remain inferable
+-- even if not in normal form.
+
+{-# OPTIONS --irrelevant-projections #-}
+{-# OPTIONS --allow-unsolved-metas #-}
+
+-- {-# OPTIONS --no-double-check #-}
+-- {-# OPTIONS -v impossible:100 #-}
+-- {-# OPTIONS -v tc:40 #-}
+
+open import Agda.Builtin.Equality
+
+record Squash {ℓ} (A : Set ℓ) : Set ℓ where
+  constructor squash
+  field
+    .unsquash : A
+open Squash
+
+.test : ∀ {ℓ} {A : Set ℓ} (x : A) (y : Squash A) → {!!}
+test x y = {!!}
+  where
+    help : unsquash (squash x) ≡ unsquash y
+    help = refl
+
+-- WAS: internal error.
+-- Should succeed with unsolved metas.