Note [Skolem abstract data]

Skolem abstract data arises from data declarations in an hsig file.

The best analogy is to interpret the types declared in signature files as
elaborating to universally quantified type variables; e.g.,

   unit p where
       signature H where
           data T
           data S
       module M where
           import H
           f :: (T ~ S) => a -> b
           f x = x

elaborates as (with some fake structural types):

   p :: forall t s. { f :: forall a b. t ~ s => a -> b }
   p = { f = \x -> x } -- ill-typed

It is clear that inside p, t ~ s is not provable (and
if we tried to write a function to cast t to s, that
would not work), but if we call p @Int @Int, clearly Int ~ Int
is provable.  The skolem variables are all distinct from
one another, but we can't make assumptions like "f is
inaccessible", because the skolem variables will get
instantiated eventually!

Skolem abstractness can apply to "non-abstract" data as well):

   unit p where
       signature H1 where
           data T = MkT
       signature H2 where
           data T = MkT
       module M where
           import qualified H1
           import qualified H2
           f :: (H1.T ~ H2.T) => a -> b
           f x = x

This is why the test is on the original name of the TyCon,
not whether it is abstract or not.