The phrase “strongly typed” does not have one single agreed upon definitions. I’ve known that for like over a decade, since it comes up extremely often when someone is upset about people not liking x language and they have to jump to semantic debates instead of debating about real problems. I assume you’re not doing that… so I can clear things up: instead of “strongly typed”, substitute in “statically typed”.

edit: Also,

> There are no gradients of strong typing

that's flatly untrue. There certainly is a notion of 'stronger' vs 'weaker'. I don't know where you got this idea from.

Huh? What do you mean by 'strongly' typed in this case?

In common parlance, there are definitely gradients.

For example compared to most mainstream languages, Haskell is strongly typed. But compared to Agda, Haskell's types are pretty weak.

For example, typically Haskell programs don't use types to enforce that you can't divide by zero. In Agda it's relatively easy to enforce that.