foo : (l : Level) -> (a : Set l) -> (x : a) -> a
foo = \(l : Level) -> \(a : Set l) -> \(x : a) -> x