Haskell for all: The appeal of bidirectional type-checking
"forall (a : Type) . a -> a is a subtype of multiple types, such as:

Integer -> Integer
List Natural -> List Natural
{ x: Bool } -> { x: Bool }
…
… and so on. This might be a bit counter-intuitive if you come from an OOP background where usually each type is a subtype of at most one other (explicitly declared) supertype."
So #dhall is more verbose? https://www.haskellforall.com/2022/06/the-appeal-of-bidirectional-type.html#:~:text=forall%20(a%20%3A%20Type)%20.%20a%20%2D%3E%20a%20is%20a%20subtype%20of%20multiple,a%20subtype%20of%20at%20most%20one%20other%20(explicitly%20declared)%20supertype.