1
{- 2010-09-28 Andreas, see issue 336 -}
3
module WhyWeNeedUntypedLambda where
5
IdT = ({A : Set} -> A -> A)
7
data _==_ {A : Set2}(a : A) : A -> Set where
12
foo : ({X : Set1} -> X -> X == IdT -> Set) -> Set
13
foo k = k (\{X} x -> x) refl -- succeeds
16
foo' : ({X : Set1} -> X -> X == IdT -> Set) -> Set
17
foo' k = k (\ (x : _) -> x) refl -- fails
b'\\ No newline at end of file'