[ fix #3073 ] Don't eta-contract \x -> f l to f when --type-in-type

src/full/Agda/TypeChecking/EtaContract.hs

@@ -111,7 +111,11 @@ etaLam i x b = do
   where
     isVar0 _ (Var 0 [])               = True
     -- Andreas, 2016-01-08 If --type-in-type, all levels are equal.
-    isVar0 True Level{}               = True
+    -- Jesper, 2019-10-15 issue #3073
+    -- Contracting level arguments is not sound unless the domain type
+    -- is in fact @Level@, e.g. @\(A : Set) → F lzero@ should not be
+    -- eta-contracted to @F@.
+    -- isVar0 True Level{}               = True
     isVar0 tyty (Level (Max 0 [Plus 0 l])) = case l of
       NeutralLevel _ v -> isVar0 tyty v
       UnreducedLevel v -> isVar0 tyty v

test/interaction/Issue3073.agda

@@ -0,0 +1,22 @@
+{-# OPTIONS --type-in-type #-}
+
+module _ where
+
+Set' : ∀ i → Set _
+Set' i = Set i
+
+postulate
+  A : Set
+  a : A
+  T : Set → Set
+  comp : (P : A → Set) (g : (a : A) → P a) → P a
+  foo : ∀ i (Q : A → Set' i) → T (comp _ Q)
+  -- (no issue if Set' is replaced by Set)
+
+bar : T {!_!} -- Try to give _
+bar = foo _ _
+
+-- WAS:
+-- A !=< Agda.Primitive.Level of type Set
+-- when checking that the expression _ has type Set
+-- SHOULD: succeed (with unsolved meta)

test/interaction/Issue3073.in

@@ -0,0 +1,2 @@
+top_command (cmd_load currentFile [])
+goal_command 0 cmd_give "_"

test/interaction/Issue3073.out

@@ -0,0 +1,10 @@
+(agda2-status-action "")
+(agda2-info-action "*Type-checking*" "" nil)
+(agda2-highlight-clear)
+(agda2-status-action "")
+(agda2-info-action "*All Goals*" "?0 : Set _Q_17 : A → Set' Agda.Primitive.lzero [ at Issue3073.agda:17,13-14 ] " nil)
+((last . 1) . (agda2-goals-action '(0)))
+(agda2-give-action 0 "_")
+(agda2-status-action "")
+(agda2-info-action "*All Goals*" "_Q_17 : A → Set' Agda.Primitive.lzero [ at Issue3073.agda:17,13-14 ] " nil)
+((last . 1) . (agda2-goals-action '()))