How can I use forall in a function definition?

user_2904322 0
Viewed 54
banana : Type
banana = forall x . x -> x

gives

While processing right hand side of banana. x is not accessible in this context.

However,

banana : Type
banana = {x : Type} -> x -> x

apple : forall x . x -> x
apple t = t

work.

How can I use universal quantification as the output of a function? If it's not possible, why not?

idris
1 Answers

forall x . means {0 x : _} -> i.e. there are no xs at runtime. Since you use x in the definition, there can be no bananas at runtime

0 banana : Type
banana : forall x . x -> x
user_59869070
Related