Rigid / skolem type variable: fine as parameter but escaping scope with local where/let statement

Per What are skolems?, this works:

{-# LANGUAGE ExistentialQuantification #-}

data AnyEq = forall a. Eq a => AE a

reflexive :: AnyEq -> Bool
reflexive (AE x) = x == x

But why doesn't this:

reflexive2 :: AnyEq -> Bool
reflexive2 ae = x == x
  where
  AE x = ae

(or the similar version with let). It produces the errors including:

Couldn't match expected type ‘p’ with actual type ‘a’
        because type variable ‘a’ would escape its scope
      This (rigid, skolem) type variable is bound by
        a pattern with constructor: AE :: forall a. Eq a => a -> AnyEq,
        in a pattern binding
        at Skolem.hs:74:4-7

Is it possible to make it work by adding some type declaration (a bit like the s :: forall a. I a -> String solution to the withContext example in that question). I feel I want to add an Eq x somewhere.

My (possibly naïve) understanding of how reflexive works is as follows:

• it takes a value of type AnyEq. This has embedded within it a value of any type provided it is an instance of Eq. This inner type is not apparent in the type signature of reflexive and is unknown when reflexive is compiled.
• The binding (AE x) = ae makes x a value of that unknown type, but known to be an instance of Eq. (So just like the variables x and y in myEq :: Eq a => a -> a -> Bool; myEq x y = x == y)
• the == operator is happy based on the implied class constraint.

I can't think why reflexive2 doesn't do the same, except for things like the "monomorphism restriction" or "mono local binds", which sometimes make things weird. I've tried compiling with all combinations of NoMonomorphismRestriction and NoMonoLocalBinds, but to no avail.

Thanks.

So I think I found the answer in the documentation (of all places!). This states:

• You can’t pattern-match on an existentially quantified constructor in a let or where group of bindings
• The reason for this restriction is really an implementation one
• We’ll see how annoying it is

There's also a request to lift the restriction (though it seems a bit challenging).

Personally, now I think I understand it, it's not that annoying. But I do think the error message generated is misleading (since I don't think the problem is scope leakage), so will request it is changed. (It would also be good if the generated error message had a reference back to the documentation, so will push my luck by asking for that too.)

Thanks all for your comments, and please let me know if you think I've got some of this wrong. David.