Explanation: Every function declares what type or kind of argument to accept For example: ┌───────────────────────────────┐ │ λ(x : Bool) → x : Bool → Bool │ This anonymous function only accepts └───────────────────────────────┘ arguments that have type ❰Bool❱ ⇧ The function's input type ┌───────────────────────────────┐ │ Natural/even : Natural → Bool │ This built-in function only accepts └───────────────────────────────┘ arguments that have type ❰Natural❱ ⇧ The function's input type ┌───────────────────────────────┐ │ λ(a : Type) → a : Type → Type │ This anonymous function only accepts └───────────────────────────────┘ arguments that have kind ❰Type❱ ⇧ The function's input kind ┌────────────────────┐ │ List : Type → Type │ This built-in function only accepts arguments that └────────────────────┘ have kind ❰Type❱ ⇧ The function's input kind For example, the following expressions are valid: ┌────────────────────────┐ │ (λ(x : Bool) → x) True │ ❰True❱ has type ❰Bool❱, which matches the type └────────────────────────┘ of argument that the anonymous function accepts ┌─────────────────┐ │ Natural/even +2 │ ❰+2❱ has type ❰Natural❱, which matches the type of └─────────────────┘ argument that the ❰Natural/even❱ function accepts, ┌────────────────────────┐ │ (λ(a : Type) → a) Bool │ ❰Bool❱ has kind ❰Type❱, which matches the kind └────────────────────────┘ of argument that the anonymous function accepts ┌───────────┐ │ List Text │ ❰Text❱ has kind ❰Type❱, which matches the kind of argument └───────────┘ that that the ❰List❱ function accepts However, you can $_NOT apply a function to the wrong type or kind of argument For example, the following expressions are not valid: ┌───────────────────────┐ │ (λ(x : Bool) → x) "A" │ ❰"A"❱ has type ❰Text❱, but the anonymous function └───────────────────────┘ expects an argument that has type ❰Bool❱ ┌──────────────────┐ │ Natural/even "A" │ ❰"A"❱ has type ❰Text❱, but the ❰Natural/even❱ function └──────────────────┘ expects an argument that has type ❰Natural❱ ┌────────────────────────┐ │ (λ(a : Type) → a) True │ ❰True❱ has type ❰Bool❱, but the anonymous └────────────────────────┘ function expects an argument of kind ❰Type❱ ┌────────┐ │ List 1 │ ❰1❱ has type ❰Integer❱, but the ❰List❱ function expects an └────────┘ argument that has kind ❰Type❱ You tried to invoke the following function: ↳ $txt0 ... which expects an argument of type or kind: ↳ $txt1 ... on the following argument: ↳ $txt2 ... which has a different type or kind: ↳ $txt3 Some common reasons why you might get this error: ● You omit a function argument by mistake: ┌────────────────────────────────────────┐ │ List/head ([1, 2, 3] : List Integer) │ └────────────────────────────────────────┘ ⇧ ❰List/head❱ is missing the first argument, which should be: ❰Integer❱ ● You supply an ❰Integer❱ literal to a function that expects a ❰Natural❱ ┌────────────────┐ │ Natural/even 2 │ └────────────────┘ ⇧ This should be ❰+2❱