Singletons TypeRepStar Sing Data Instance

I'm new to Haskell, so I'm probably missing something obvious, but what seems to be the problem here?

The singletons library provides a Sing instance for the kind * in import Data.Singletons.TypeRepStar.

The Sing data family is defined as follows..

data family Sing (a :: k)

and the * instance is defined as..

data instance Sing (a :: *) where
  STypeRep :: Typeable a => Sing a

I'm trying to reproduce a minimal version of this using the following ...

{-# LANGUAGE GADTs
           , TypeFamilies
           , PolyKinds
           #-}

module Main where

import Data.Typeable

data family Bloop (a :: k)
data instance Bloop (a :: *) where
  Blop :: Typeable a => Bloop a

main :: IO ()
main = putStrLn "Hello, Haskell!"

But I'm getting the following error...

Main.hs:12:3: error:
    • Data constructor ‘Blop’ returns type ‘Bloop a’
         instead of an instance of its parent type ‘Bloop a’
    • In the definition of data constructor ‘Blop’
         In the data instance declaration for ‘Bloop’
    |
 12 |   Blop :: Typeable a => Bloop a
    |   ^

Solution

The compiler insists that the a in Bloop (a :: *) and the a in Typeable a => Bloop a are not the same a. It produces exactly the same error if you replace one of them with b:

data instance Bloop (b :: *) where
      Blop :: Typeable a => Bloop a

* Data constructor `Blop' returns type `Bloop a'
    instead of an instance of its parent type `Bloop b'
* In the definition of data constructor `Blop'
  In the data instance declaration for `Bloop'

This can be made more visible with -fprint-explicit-kinds:

* Data constructor `Blop' returns type `Bloop k a'
    instead of an instance of its parent type `Bloop * a'
* In the definition of data constructor `Blop'
  In the data instance declaration for `Bloop'

Now we can clearly see right in the error message that one a has kind k and the other has kind *. From this, a solution is obvious - explicitly declare the kind of the second a :

data instance Bloop (a :: *) where
      Blop :: Typeable (a :: *) => Bloop (a :: *)  -- Works now

It appears that this happens because of the PolyKinds extension. Without it, the second a is assumed to have kind *, and thus the original definition works.