I don’t have much experience with it, but here is an example of how they differ:
> :k Eq ~ Int
<interactive>:1:6: error:
• Expected kind ‘* > Constraint’, but ‘Int’ has kind ‘*’
• In the second argument of ‘(~)’, namely ‘Int’
In the type ‘Eq ~ Int’
> :k Eq ~~ Int
Eq ~~ Int :: Constraint
So you can use ~~ with types that have different kinds.
The second example MkFoo1 :: Int => ... doesn’t make sense to me, because Int is a type and not a constraint, so it cannot appear on its own on the left of the constraint arrow =>. You will get an error:
> :k Int => Int
<interactive>:1:1: error:
• Expected a constraint, but ‘Int’ has kind ‘*’
• In the type ‘Int => Int’
Edit: Oh, I think you meant a ~~ Int => ..., in that case there is no real difference in that particular example, but you can write more things, like:
> :set XTypeOperators
> :set XTypeFamilies
> :set XKindSignatures
> :set XExplicitForAll
> import GHC.Types
> :k forall (a :: *). a ~ Eq => a
<interactive>:1:22: error:
• Expecting one more argument to ‘Eq’
Expected a type, but ‘Eq’ has kind ‘* > Constraint’
• In the second argument of ‘(~)’, namely ‘Eq’
In the type ‘forall (a :: *). a ~ Eq => a’
> :k forall (a :: *). a ~ Eq => a
forall (a :: *). a ~~ Eq => a :: *
I would have expected to be able to write:
{# LANGUAGE TypeOperators, TypeFamilies, ExplicitForAll, KindSignatures #}
import GHC.Types
x :: forall (a :: *). a ~~ Eq => a
x = undefined
But, I’m getting an error:
[1 of 1] Compiling Main ( Test.hs, interpreted )
Test.hs:5:6: error:
• Couldn't match kind ‘* > Constraint’ with ‘*’
When matching types
a :: *
Eq :: * > Constraint
• In the ambiguity check for ‘x’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature: x :: forall (a :: *). a ~~ Eq => a

5  x :: forall (a :: *). a ~~ Eq => a
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^