Господа, копаюсь вот в Data.Constraint и увидел там занимательнный тип newtype

Question

Господа, копаюсь вот в Data.Constraint и увидел там занимательнный тип newtype

a :- b
где :k a :: Constraint и :k b :: Constraint
Судя по описанию, он представляет собой следование, то есть "имеем в скоупе констрейнт a, значит имеем констрейнт b"
и наличие объекта типа :- означает что мы имеем в скоупе констрейнт b

я не могу придумать другого случая следования кроме как
class (Eq a) => Ord a
И по идее по дефолту должно выполняться, что Ord a :- Eq a , зачем для пруфа этого факта нужен отдельный тип? Разве если у нас в скоупе есть Ord a, не значит ли это что есть Eq a?

помимо этого решил немного поиграться и ручками создать экземпляр :- для игрушечных тайпклассов
class A a where
class (A a) => B a where

instance A Int
instance B Int

proof :: B Int :- A Int
proof = ???
но понял что не совсем понимаю как его создать, ибо вид конструктора :-`меня смущает -- `Sub (a => Dict b) , а именно смущает наличие толстой стрелки внутри скобок