Vera's type variables are currently unconstrained (forall<T>). To support practical generic programming — sorting, hashing, serialisation — type variables need constraints. Vera should adopt Roc-style restricted abilities rather than full Haskell-style typeclasses:

ability Eq<T> {
  op eq(@T, @T -> @Bool);
}

ability Ord<T> {
  op compare(@T, @T -> @Ordering);
}

forall<T where Eq<T>> fn contains(@Array<T>, @T -> @Bool)
  requires(true)
  ensures(true)
  effects(pure)
{
  exists(@Nat, length(@Array<T>.0), fn(@Nat -> @Bool) effects(pure) {
    eq(@Array<T>.0[@Nat.0], @T.0)
  })
}

Key design points:

• No higher-kinded types. No Functor, Monad, Applicative. Abilities are first-order only.
• Built-in abilities auto-derivable for ADTs: Eq, Ord, Hash, Encode, Decode, Show.
• User-defined abilities permitted but restricted to first-order type parameters.
• Constraint syntax uses forall<T where Ability<T>>.

Post-v0.1 feature. Will be specified in Chapter 2 when implemented.

Spec reference: spec/00-introduction.md § 0.8 "Abilities (Restricted Type Constraints)"