Strange interaction between TypeAbstractions and equality constraints

The following declarations are both accepted by GHC and our formalism:

{-# LANGUAGE TypeAbstractions #-}

f1 :: forall a. a ~ Int => a -> Bool
f1 @a x = True

f2 :: forall a. a ~ Int => a -> Bool
f2 @Int x = True 

The latter -- although type-safe -- is very strange to accept.

When |-match calls |-skolapats with our kindchecked quantifiers and their corresponding argument patterns -- where kindchecked quantifiers =(forall alpha : Type.), (alpha ~ Int), (alpha ->), and argument patterns = @Int, x -- we'll get a Delta containing alpha ~ Int as a given, and a list of wanteds which contains the same constraint, but this time as a wanted.

i.e: Gamma |-skolapats (forall alpha : Type.), (alpha ~ Int), (alpha ->) ; (@Int, x) ~> < x ; a > ; (alpha : Type, alpha ~ Int) ; alpha ~ Int

Then later on, in the third premise of the rule Match-Check, we'll extend Gamma with (alpha : Type, alpha ~ Int) and try to prove the wanted constraints; which in this case, is comprised solely of alpha ~ Int.

i.e: Gamma, alpha : Type, alpha ~ Int ||- alpha ~ Int

The responsible rules are: Match-Check, SkolAPats-Specified, and SkolAPats-Constraint.