#7105 Do not try to fold let-bindings during printing of the helper f…

…unction

src/full/Agda/Interaction/BasicOps.hs

@@ -977,7 +977,12 @@ metaHelperType norm ii rng s = case words s of
     -- Konstantin, 2022-10-23: We don't want to print section parameters in helper type.
     freeVars <- getCurrentModuleFreeVars
     contextForAbstracting <- drop freeVars . reverse <$> getContext
-    let escapeAbstractedContext = escapeContext impossible (length contextForAbstracting)
+
+    -- Andreas, 2019-10-11: I actually prefer pi-types over ->.
+    let runInPrintingEnvironment = localTC (\e -> e { envPrintDomainFreePi = True, envPrintMetasBare = True })
+                                 . escapeContext impossible (length contextForAbstracting)
+                                 . withoutPrintingGeneralization
+                                 . dontFoldLetBindings
 
     case mapM (isVar . namedArg) args >>= \ xs -> xs <$ guard (all inCxt xs) of
 
@@ -989,9 +994,7 @@ metaHelperType norm ii rng s = case words s of
       let hideButXs dom = setHiding (if inXs $ fst $ unDom dom then NotHidden else Hidden) dom
       let tel = telFromList . map (fmap (first nameToArgName) . hideButXs) $ contextForAbstracting
       OfType' h <$> do
-        -- Andreas, 2019-10-11: I actually prefer pi-types over ->.
-        localTC (\e -> e { envPrintDomainFreePi = True }) $ escapeAbstractedContext $ withoutPrintingGeneralization $
-          reify $ telePiVisible tel a0
+        runInPrintingEnvironment $ reify $ telePiVisible tel a0
 
      -- If some arguments are not variables.
      Nothing -> do
@@ -1004,7 +1007,7 @@ metaHelperType norm ii rng s = case words s of
       TelV atel _ <- telView a
       let arity = size atel
           (delta1, delta2, _, a', vtys') = splitTelForWith tel a vtys
-      a <- localTC (\e -> e { envPrintDomainFreePi = True, envPrintMetasBare = True }) $ escapeAbstractedContext $ withoutPrintingGeneralization $ do
+      a <- runInPrintingEnvironment $ do
         reify =<< cleanupType arity args =<< normalForm norm =<< fst <$> withFunctionType delta1 vtys' delta2 a' []
       reportSDoc "interaction.helper" 10 $ TP.vcat $
         let extractOtherType = \case { OtherType a -> a; _ -> __IMPOSSIBLE__ } in

test/interaction/Issue7105.agda

@@ -0,0 +1,12 @@
+open import Agda.Primitive renaming (Set to Type)
+open import Agda.Builtin.Sigma
+
+postulate
+  ℕ : Type
+
+data T (n : ℕ) : Type where
+  conv : ∀ m → T m → T n
+
+test : ∀ n → T n → Σ ℕ T
+test n (conv m t) = let n' , t' = test m t in {!helper t'!}  -- C-c C-h
+

test/interaction/Issue7105.in

@@ -0,0 +1,2 @@
+top_command (cmd_load currentFile [])
+goal_command 0 (cmd_helper_function AsIs) "helper"

test/interaction/Issue7105.out

@@ -0,0 +1,8 @@
+(agda2-status-action "")
+(agda2-info-action "*Type-checking*" "" nil)
+(agda2-highlight-clear)
+(agda2-status-action "")
+(agda2-info-action "*All Goals*" "?0 : Σ ℕ T " nil)
+((last . 1) . (agda2-goals-action '(0)))
+(agda2-status-action "")
+(agda2-info-action-and-copy "*Helper function*" "helper : Σ ℕ T " nil)