idris-1.3.0: test/regression002/reg001.idr

foo : (a : Type) -> (b : Type) -> a -> b
foo a a x = x