Fix agda#7148: restore call to instantiateFull before with-abstract…

…ion.

Regression introduced in agda#7122.

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

@@ -1570,7 +1570,11 @@ inferExprForWith (Arg info e) = verboseBracket "tc.with.infer" 20 "inferExprForW
     reportSDoc "tc.with.infer" 20 $ "inferExprforWith " <+> prettyTCM e
     reportSLn  "tc.with.infer" 80 $ "inferExprforWith " ++ show (deepUnscope e)
     traceCall (InferExpr e) $ do
-      (v, t) <- inferExpr e
+      -- Andreas, 2024-02-26, issue #7148:
+      -- The 'instantiateFull' here performs necessary eta-contraction,
+      -- both for future with-abstraction,
+      -- and for testing whether v is a variable modulo eta.
+      (v, t) <- instantiateFull =<< inferExpr e
       v <- reduce v
       -- Andreas 2014-11-06, issue 1342.
       -- Check that we do not `with` on a module parameter!

test/Fail/Issue1342b.agda

@@ -0,0 +1,63 @@
+-- Andreas, 2024-02-26, issue #7148 brings back #1342.
+-- We are not supposed to match on a module parameter,
+-- even when it is given in eta-expanded form.
+
+open import Agda.Builtin.Equality
+
+data One : Set where
+  one : One
+
+record Wrap (A : Set) : Set where
+  constructor wrap
+  field wrapped : A
+open Wrap
+
+Unit = Wrap One
+pattern unit = wrap one
+
+id : (A : Set) → A → A
+id A a = a
+
+module Works where
+
+  dx : (x : Unit) → Unit → Unit
+  dx x unit = x
+
+  g : (x : Unit) → ∀ u → x ≡ dx x u
+  g x with wrap (wrapped x)
+  g x | unit = id ((u : Unit) → unit ≡ dx unit u) {!!}
+
+-- Now if we make (x : Unit) a module parameter
+-- then we turn all applications (dx _) into just dx,
+-- which actually means (dx x), i.e., dx applied to
+-- the module free variables.
+
+-- This leads to an incomprehendable rejection
+-- of the following code (culprit is the first argument to id).
+
+module M (x : Unit) where
+
+  dx : Unit → Unit
+  dx unit = x
+
+  g : ∀ u → x ≡ dx u
+  -- As well as rejecting `with x` we should also
+  -- reject `with (eta-expansion-of x)`.
+  g with wrap (wrapped x)
+  g | unit  = id ((u : Unit) → unit ≡ dx u) ?
+
+-- Error WAS:
+--
+-- wrapped x != one of type One
+-- when checking that the inferred type of an application
+--   (u : Unit) → unit ≡ dx u
+-- matches the expected type
+--   (u : Wrap One) → unit ≡ dx u
+--
+-- Expected error NOW:
+--
+-- Cannot `with` on expression wrap (wrapped x) which reduces to
+-- variable x bound in a module telescope (or patterns of a parent clause)
+-- when inferring the type of wrap (wrapped x)
+
+-- -}

test/Fail/Issue1342b.err

@@ -0,0 +1,5 @@
+Issue1342b.agda:46,10-26
+Cannot 'with' on expression wrap (wrapped x) which reduces to
+variable x bound in a module telescope (or patterns of a parent
+clause)
+when inferring the type of wrap (wrapped x)

test/Fail/Issue2324.agda

@@ -1,3 +1,5 @@
+-- Issue #2324
+-- Prevent 'with' on a module parameter through the backdoor.
 
 Type-of : {A : Set} → A → Set
 Type-of {A = A} _ = A
@@ -7,3 +9,9 @@ module _ (A : Set) where
   Foo : A → Set
   Foo a with Type-of a
   ... | B = B
+
+-- Should fail.  Expected error:
+--
+-- Cannot 'with' on expression Type-of a which reduces to variable A
+-- bound in a module telescope (or patterns of a parent clause)
+-- when inferring the type of Type-of a

test/Fail/Issue2324.err

@@ -1,4 +1,4 @@
-Issue2324.agda:8,14-23
+Issue2324.agda:10,14-23
 Cannot 'with' on expression Type-of a which reduces to variable A
 bound in a module telescope (or patterns of a parent clause)
 when inferring the type of Type-of a

test/Fail/Issue7148a.agda

@@ -0,0 +1,10 @@
+-- Andreas, 2024-02-26, issue #7148.
+-- See also #1342.
+
+module _ (A : Set) (a : A → A) where
+
+test : Set
+test with (λ (x : A) → a x)
+... | _ = A
+
+-- Should fail as we cannot with-abstract over module parameter.

test/Fail/Issue7148a.err

@@ -0,0 +1,5 @@
+Issue7148a.agda:7,12-27
+Cannot 'with' on expression λ (x : A) → a x which reduces to
+variable a bound in a module telescope (or patterns of a parent
+clause)
+when inferring the type of λ (x : A) → a x

test/Succeed/Issue7148.agda

@@ -0,0 +1,39 @@
+-- Andreas, 2024-02-26, issue #7148, regression in 2.6.4.2.
+-- Original test case by mechvel.
+-- 'with'-abstraction failed here due to lack of eta-contraction.
+
+data _≡_ {A : Set} (x : A) : A → Set where
+  refl : x ≡ x
+
+record Wrap (A : Set) : Set where
+  -- pattern; no-eta-equality   -- can't turn off eta
+  constructor wrap
+  field wrapped : A
+
+data Dec (A : Set) : Set where
+  no : Dec A
+
+postulate
+  foo : ∀{A : Set}{P : A → Set} → (∀ x → Dec (P x)) → ∀ x → Dec (P x)
+    -- can't inline P = LtWrap
+    -- can't define foo = id
+  Nat : Set
+  P   : Nat → Set
+  p?  : ∀ x → Dec (P x)
+
+-- can't make these postulates
+PWrap : Wrap Nat → Set
+PWrap (wrap f) = P f
+
+pWrap? : ∀ p → Dec (PWrap p)
+pWrap? (wrap f) = p? f
+
+bar : Wrap Nat → Wrap Nat
+bar fs with foo pWrap? fs
+... | no = fs
+
+test : ∀ fs → bar fs ≡ fs
+test fs with foo pWrap? fs
+... | no = refl
+
+-- Should succeed.