GHC does not respect semantics of bang patterns

If I write

a :: forall a. a -> a
a = let y :: Eq a => a
        !y = undefined
    in \z -> z

and evaluate a True, I get True. This is surprising -- I expected to see an exception thrown. The problem is that GHC does not instantiate y before forcing it. y is a function from Eq a to a, and thus is a value.

Yet https://gitlab.haskell.org/haskell/prime/-/wikis/BangPatterns describes the desugaring of the above to be

a :: forall a. a -> a
a = let y :: Eq a => a
        y = undefined
    in y `seq` \z -> z

which does not compile, as there is no Eq a instance. I think we should stick to the specification here and reject both programs. This means that GHC will struggle to support a strict binding of a polymorphic value, but I think that's appropriate, as I would want users to be careful in this corner and say exactly what they mean, lest they get surprised by GHC's behavior.