Hécate:

* Type variables are made explicit, and as such I annotate even the simplest of them (with `:: Type`)

This! I am moving towards that style. Especially in teaching (type abstraction, type application) where I want everything to be very much explicit - before discussing abbreviations and omissions (type inference). With current GHC, this is entirely possible but looks somewhat clumsy {-# language ExplicitForall, KindSignatures #-} import Data.Kind (Type) g :: forall (t :: Type) . t -> t ; g x = x {-# language TypeApplications #-} g @N Z yes I could hide these pragmas somewhere but that again feels wrong. But - good thing: after https://github.com/ghc-proposals/ghc-proposals/blob/ghc2021/proposals/0000-g... (I understand that GHC2021 is default-enabled in GHC-9.2) we no longer need to write these pragmas. Yay! Sadly, we still need the import. - J. NB: Haskell's implicit declaration of type variables by their starting with lowercase letters always reminds me of Fortran's implicit type specification for variables, going by the first letter (I .. N means integer). Fortran has "implicit none" though, so let's have "t :: Type"...