Eta-contraction is not type-preserving #2732
Description
Agda version 2.6.0-75e13d3-dirty
open import Data.Nat using (ℕ; zero)
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Level using (_⊔_) renaming (suc to lsuc)
module Bug where
record R a b : Set (lsuc a ⊔ b) where
field
f : Set a
module Inner {a b} {r : R a b} where
r2 : R a (lsuc b)
r2 = record { f = R.f r}
module Inner2 {a b} (r : R a b) where
postulate n : ℕ
open Inner2 r2
test : n ≡ n
test with zero
... | c = {!!}Type checking triggers the error:
Set b != Set (lsuc b)
when checking that the type
ℕ → {a b : Level.Level} {r : R a b} → Inner2.n r ≡ Inner2.n r of
the generated with function is well-formed
Compiles fine when you remove the with clause in test with
test : n ≡ n
test = ?