Unspine system projections when they have display forms (#7055)

* Unspine system projections when they have display forms

* fixup: get rid of nasty unsafePerformIO

src/full/Agda/Syntax/Internal.hs

@@ -1049,12 +1049,12 @@ suggests (Suggestion x : xs) = fromMaybe (suggests xs) $ suggestName x
 
 -- | Convert top-level postfix projections into prefix projections.
 unSpine :: Term -> Term
-unSpine = unSpine' $ const True
+unSpine = unSpine' $ \_ _ -> True
 
 -- | Convert 'Proj' projection eliminations
 --   according to their 'ProjOrigin' into
 --   'Def' projection applications.
-unSpine' :: (ProjOrigin -> Bool) -> Term -> Term
+unSpine' :: (ProjOrigin -> QName -> Bool) -> Term -> Term
 unSpine' p v =
   case hasElims v of
     Just (h, es) -> loop h [] es
@@ -1063,9 +1063,9 @@ unSpine' p v =
     loop :: (Elims -> Term) -> Elims -> Elims -> Term
     loop h res es =
       case es of
-        []                   -> v
-        Proj o f : es' | p o -> loop (Def f) [Apply (defaultArg v)] es'
-        e        : es'       -> loop h (e : res) es'
+        []                     -> v
+        Proj o f : es' | p o f -> loop (Def f) [Apply (defaultArg v)] es'
+        e        : es'         -> loop h (e : res) es'
       where v = h $ reverse res
 
 -- | A view distinguishing the neutrals @Var@, @Def@, and @MetaV@ which

src/full/Agda/Syntax/Translation/InternalToAbstract.hs

@@ -481,12 +481,21 @@ reifyTerm expandAnonDefs0 v0 = tryReifyAsLetBinding v0 $ do
   -- Ulf 2014-07-10: Don't expand anonymous when display forms are disabled
   -- (i.e. when we don't care about nice printing)
   expandAnonDefs <- return expandAnonDefs0 `and2M` displayFormsEnabled
+
   -- Andreas, 2016-07-21 if --postfix-projections
   -- then we print system-generated projections as postfix, else prefix.
   havePfp <- optPostfixProjections <$> pragmaOptions
-  let pred = if havePfp then (== ProjPrefix) else (/= ProjPostfix)
-  reportSDoc "reify.term" 80 $ pure $ "reifyTerm (unSpine v) = " <+> pretty (unSpine' pred v)
-  case unSpine' pred v of
+
+  -- Amy, 2024-01-07: postfix and system projections should still be
+  -- turned into head symbols *if* they have display forms attached.
+  hasDisplay <- liftReduce $ unKleisli hasDisplayForms
+  let
+    prefixize orig name
+      | havePfp   = (orig == ProjPrefix)  || hasDisplay name
+      | otherwise = (orig /= ProjPostfix) || hasDisplay name
+  reportSDoc "reify.term" 80 $ pure $ "reifyTerm (unSpine v) = " <+> pretty (unSpine' prefixize v)
+
+  case unSpine' prefixize v of
     -- Hack to print generalized field projections with nicer names. Should
     -- only show up in errors. Check the spined form!
     _ | I.Var n (I.Proj _ p : es) <- v,

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

@@ -4872,6 +4872,8 @@ reduceSt f s = f (redSt s) <&> \ e -> s { redSt = e }
 newtype ReduceM a = ReduceM { unReduceM :: ReduceEnv -> a }
 --  deriving (Functor, Applicative, Monad)
 
+unKleisli :: (a -> ReduceM b) -> ReduceM (a -> b)
+unKleisli f = ReduceM $ \ env x -> unReduceM (f x) env
 
 onReduceEnv :: (ReduceEnv -> ReduceEnv) -> ReduceM a -> ReduceM a
 onReduceEnv f (ReduceM m) = ReduceM (m . f)

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

@@ -743,6 +743,9 @@ getDisplayForms q = do
   ifM (isLocal q) (return $ ds ++ ds1 ++ ds2)
                   (return $ ds1 ++ ds ++ ds2)
 
+hasDisplayForms :: (HasConstInfo m, ReadTCState m) => QName -> m Bool
+hasDisplayForms = fmap (not . null) . getDisplayForms
+
 -- | Find all names used (recursively) by display forms of a given name.
 chaseDisplayForms :: QName -> TCM (Set QName)
 chaseDisplayForms q = go Set.empty [q]

src/full/Agda/TypeChecking/Reduce/Fast.hs

@@ -467,9 +467,6 @@ fastReduce' norm v = do
     compactDef bEnv info rewr
   ReduceM $ \ redEnv -> reduceTm redEnv bEnv (memoQName constInfo) norm v
 
-unKleisli :: (a -> ReduceM b) -> ReduceM (a -> b)
-unKleisli f = ReduceM $ \ env x -> unReduceM (f x) env
-
 -- * Closures
 
 -- | The abstract machine represents terms as closures containing a 'Term', an environment, and a

test/Fail/PostfixProjDisplay.agda

@@ -0,0 +1,25 @@
+{-# OPTIONS --postfix-projections #-}
+module PostfixProjDisplay where
+
+open import Agda.Builtin.Equality
+
+postulate
+  A : Set
+  a : A
+
+record Foo : Set where
+  field
+    _+_ : A → A → A
+
+record Bar : Set where
+  field
+    foo : Foo
+  open Foo foo public
+
+module M1 (X : Bar) where
+  open Bar X
+
+  -- Error message should show a + a
+  -- Used to show foo .Foo._+_ a a
+  it : a + a ≡ a
+  it = refl

test/Fail/PostfixProjDisplay.err

@@ -0,0 +1,3 @@
+PostfixProjDisplay.agda:25,8-12
+a + a != a of type A
+when checking that the expression refl has type (a + a) ≡ a