type-in-type and spurious levels

[sattlerc]

I know the current implementation has been described as a hack, so probably this bug is known.

{-# OPTIONS --type-in-type #-}
module Strange 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 {!_!}
bar = foo _ _

Giving the underscore at the interaction point yields the following error message:

A !=< .Agda.Primitive.Level of type Set
when checking that the expression _ has type Set

This looks like some de Brujin index mismatch.

[jespercockx]

The cause seems to be in the call to etaOnce in instantiateFull: this is eta-contracting \(A : Set) -> Set' lzero to Set', which is absolutely wrong. The check that the type of the domain is indeed Level is simply missing. However, it is not easy to add it because instantiateFull is not type-directed. Instead, I will try to remove it and see if anything breaks.

[jespercockx]

Removing the ill-typed eta-contraction did not break anything in the test suite, so I went ahead and pushed it.