TypeRep in data type does not work with genSingletons.

[Sintrastes]

With singletons-3.0 and singletons-th-3.0, if I try to generate a singled data type with TypeRep as one of the fields, with genSingletons, for instance:

data MvType s where
  MvHsT   :: TypeRep -> MvType s
  MvBaseT :: s -> MvType s
  MvFunT  :: MvType s -> MvType s -> MvType s
  MvPredT :: MvType s

$(genSingletons [''MvType])

I get the following exception in GHC:

src/Meriv/Types.hs:27:2: error:
    • Couldn't match type ‘Demote
                             base-4.15.0.0:Data.Typeable.Internal.SomeTypeRep’
                     with ‘base-4.15.0.0:Data.Typeable.Internal.SomeTypeRep’
      Expected: TypeRep
        Actual: Demote base-4.15.0.0:Data.Typeable.Internal.SomeTypeRep
    • When checking that the pattern signature:
          Demote base-4.15.0.0:Data.Typeable.Internal.SomeTypeRep
        fits the type of its context: TypeRep
      In the pattern:
        b_a7uB :: Demote base-4.15.0.0:Data.Typeable.Internal.SomeTypeRep
      In the pattern:
        MvHsT (b_a7uB :: Demote base-4.15.0.0:Data.Typeable.Internal.SomeTypeRep)
   |

I know that there are issues with TypeRep promotion, as documented here, however, I was not able to find any documentation explaining how to use Data.Singletons.Base.TypeRepTYPE to create a singled version of a data type containing TypeRep.

Note: a related issue looks like it had a workaround added in 3.0 so genSingletons works correctly with data types with Nats, so I am wondering if it is possible to add a workaround for TypeRep as well.

[RyanGlScott]

Indeed, singletons does not automatically promote TypeRep to Type. There is a workaround for situations where one wishes to promote to a from a term-level thing to a type-level thing when the two things are very similar, as described in this section of the README. For instance, you can promote from Text to Symbol, since the API for the two types can be unified with the OverloadedStrings extension (at least, to some extent).

TypeRep and Type are not quite as similar to each other as, say, Text and Symbol, so it would be trickier to figure out how to use the same workaround to promote TypeRep to Type. It might depend on what your intended use case is.

[Sintrastes]

My use case is to use MvType s as the kind of types for an EDSL, with expressions of type MvTerm s (t :: MvType s) -- but I also want to be able to inject Haskell expressions of arbitrary type into this EDSL. MvHsT rep is the type of MvTerms of Haskell type rep (where rep is a type rep).

I then have a constructor whose type looks like:

HsTerm :: Typeable a => a -> MvTerm s ('MvHsT typeRep)

to build up raw haskell expressions embedded into my EDSL.

[RyanGlScott]

Ah, OK, so you want to use the typeRep function as the way to construct TypeReps at the term level, and Types and the type level? In that case, what might work (emphasis on "might", as I haven't tried this myself) is to define a type-level version of the typeRep function:

type TypeRep :: proxy a -> Type
type family TypeRep pa where
  TypeRep @proxy @a _ = a

Then you'd need a separate, type-level-only version of MvType where the MvHsT constructor's counterpart has a Type field instead of a TypeRep. Then, using the tricks described in this section of the README, implement a custom promotion scheme that promotes the term-level MvType to your new type-level one. If you do that, then something like $(promote [d| f = MvHsT (typeRep (Proxy @Bool)) |]) might work. Again, might.

If this seems rather ugly, it's because it is. But this is the current state of things.