let f : (a → a) → a → a = λg. λx. g(g(x)) in f(λx. x + x) : ℕ → ℕ
let f : (a → a) → a → a = λg. λx. g(g(x)) in f(λx. x - x) : ℤ → ℤ
let f : (a → a) → a → a = λg. λx. g(g(x)) in f(λx. x / x) : 𝔽 → 𝔽
let f : (a → a) → a → a = λg. λx. g(g(x)) in f(λx. -x / x) : ℚ → ℚ
λx. x : a → a
λx. λy. x : a1 → a → a1
λx. λy. λz. x + y + z : ℕ → ℕ → ℕ → ℕ
λx. λy : ℕ. x - y : ℤ → ℕ → ℤ
λw. λx : ℕ. λy. λz : 𝔽. w - x + y + z : ℚ → ℕ → ℚ → 𝔽 → ℚ
Error: typechecking failed.
https://disco-lang.readthedocs.io/en/latest/reference/typecheck-fail.html