Problems
Reflection for variant types causes code duplication
?(???)?bool??(?f. ?x. f @ (f @ (f @ (if x then y else z)))) = ?f. ?x. if x then f @ (f @ (f @ (y))) = ?f. ?x. if x else f @ (f @ (f @ (z)))
Reflection for primitive/inductive types is impossible
?int?int (?n. 1 + 2 + n) = ???
?int_list?int_list (?a. (tl (tl (3 :: a))) = ???