Open Sintrastes opened 2 years ago
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.
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 MvTerm
s 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.
Ah, OK, so you want to use the typeRep
function as the way to construct TypeReps
at the term level, and Type
s 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.
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, withgenSingletons
, for instance:I get the following exception in GHC:
I know that there are issues with
TypeRep
promotion, as documented here, however, I was not able to find any documentation explaining how to useData.Singletons.Base.TypeRepTYPE
to create a singled version of a data type containingTypeRep
.Note: a related issue looks like it had a workaround added in 3.0 so
genSingletons
works correctly with data types withNat
s, so I am wondering if it is possible to add a workaround forTypeRep
as well.