a !
     : Foo
where
?y : [ |- nat]
a !
     : Foo
a
     : Foo -> Foo
a !
     : Foo