Singletons TypeRepStar Sing Data Instance

Question

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
    |   ^

Answer 1

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.

Answer 2

It appears as though the PolyKinds extension is causing the error. The singletons library splits the data family declaration and the data instance definitions into different files. The data family requires the PolyKinds extension to work, but if the instance will fail if the extension is on. It seems you must use the KindSignatures extension instead.

Def.hs

{-# LANGUAGE PolyKinds, TypeFamilies #-}

module Def (Bloop) where

data family Bloop (a :: k)

Main.hs

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

module Main where

import Def
import Data.Typeable

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

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