VarBug.agda

-- Is this a bug in Agda?
-- Try repro with latest agda sometime

module VarBug where

open import Agda.Builtin.Equality
open import Agda.Primitive

data Unit : Set where
  tt : Unit

_~>_ : {l : Level} → Unit → Set l → Set l
tt ~> S = S

wrap : {A : Unit} {l : Level} {S : Set l} → S → (A ~> S)
wrap {tt} x = x

wrap-id : {l : Level} {S : Set l} (x : S) → wrap x ≡ x
wrap-id x = refl

variable
  l : Level
  S : Set l

wrap-id' : (x : S) → wrap x ≡ x
wrap-id' x = refl