Maybe there is a better way of achieving what I want, but this is my current attempt.

I am working with the singletons package in order to reify values into types. This works fine, but at some point I will have to run a function that is polymorphic in the reified type and expects it to have a Typeable instance. Of course, all types in Haskell have such instances (at least afaik?), but since the type variable is unknown at compile time, the type checker can't find such an instance. Let me illustrate:

{-# LANGUAGE GADTs, FlexibleInstances, RankNTypes, PolyKinds, TypeFamilyDependencies, InstanceSigs #-}

import Data.ByteString (ByteString)
import Data.Typeable (Typeable)
import Data.Singletons

-- The unreified type.
data EType
  = Integer
  | Boolean
  | ByteStr
  deriving (Eq, Ord, Show, Read)

-- The corresponding singleton types.
-- Note that the parameter piggybacks
-- on Haskell's regular types.
data SType a where
  SInteger :: SType Int
  SBoolean :: SType Bool
  SByteStr :: SType ByteString

-- My singleton types are singletons.
type instance Sing = SType

-- Makes it possible to reify `EType` into `Int`,
-- `Bool` and `ByteString`, and to reflect back
-- from them to `EType`.
instance SingKind * where
  type Demote * = EType
           
           -- SType a       -> EType 
  fromSing :: Sing (a :: *) -> Demote *
  fromSing SInteger = Integer
  fromSing SBoolean = Boolean
  fromSing SByteStr = ByteStr

         -- EType    -> SomeSing *
  toSing :: Demote * -> SomeSing *
  toSing Integer = SomeSing SInteger
  toSing Boolean = SomeSing SBoolean
  toSing ByteStr = SomeSing SByteStr

-- Some dummy types for illustration.
-- Should be self-explanatory.
data UntypedExp
data Exp a
data Result

-- The function I actually want to implement.
checkResult :: EType -> UntypedExp -> Maybe Result
checkResult typ expr = withSomeSing typ $ \singType ->
  makeResult singType <$> inferExpr expr

-- A version of my main type checking function (some 
-- inputs omitted). The caller chooses `a`, and
-- depending on whether the input can be typed in
-- that way or not, we return `Just e` or `Nothing`.
-- THIS IS ALREADY IMPLEMENTED.
inferExpr :: Typeable a => UntypedExp -> Maybe (Exp a)
inferExpr = undefined

-- Depending on `a`, this function needs to do
-- different things to construct a `Result`.
-- Hence the reification.
-- THIS IS ALREADY IMPLEMENTED.
makeResult :: Sing a -> Exp a -> Result
makeResult = undefined

This gives me the error

    • No instance for (Typeable a) arising from a use of ‘inferExpr’
    • In the second argument of ‘(<$>)’, namely ‘inferExpr expr’
      In the expression: makeResult singType <$> inferExpr expr
      In the second argument of ‘($)’, namely
        ‘\ singType -> makeResult singType <$> inferExpr expr’
   |
54 |   makeResult singType <$> inferExpr expr
   |                           ^^^^^^^^^^^^^^

Which makes perfect sense. withSomeSing doesn't guarantee that the Sing a passed to the continuation satisfies Typeable a.

I can fix this, by hiding some imports from Data.Singleton and instead defining my own versions with the relevant constraint:

import Data.Singletons hiding (SomeSing,SingKind(..),withSomeSing)

withSomeSing :: forall k r
              . SingKind k
             => Demote k                          
             -> (forall (a :: k). Typeable a => Sing a -> r)
             -> r
withSomeSing x f =
  case toSing x of
    SomeSing x' -> f x'

class SingKind k where
  type Demote k = (r :: *) | r -> k
  fromSing :: Sing (a :: k) -> Demote k
  toSing   :: Demote k -> SomeSing k

data SomeSing k where
  SomeSing :: Typeable a => Sing (a :: k) -> SomeSing k

This makes everything work, but feels like absolutely terrible style.

Hence my question: is there any way of importing the original definitions of SomeSing and withSomeSing, but augment their types with this additional constraint? Or, how would you suggest solving this problem in a better way?

CodePudding user response：

Two options spring to mind:

1. Implement

    withTypeable :: SType a -> (Typeable a => r) -> r
   

   via exhaustive pattern matching on the first argument. Then instead of just withSomeSing, you use both, as in withSomeSing typ $ \singType -> withTypeable singType $ ....

2. Upgrade your Sing instance. Write

    data STypeable a where STypeable :: Typeable a => SType a -> STypeable a
    type instance Sing = STypeable
   

   You will need to throw an extra STypeable constructor in each branch of toSing and fromSing. Then you can pattern match in withSomeSing, as in withSomeSing $ \(STypeable singType) -> ....

There are likely other ways, too.

CodePudding user response：

You can avoid the CPS style entirely. Any time I see (Cls a => res) -> res I prefer to use pattern matching.

singletons has pattern FromSing which replaces withSomeSing with a pattern match:

checkResult :: EType -> UntypedExp -> Maybe Result
checkResult (FromSing (singType :: SType a)) expr = ..

Then you define a way to get a Typeable constraint from SType. For these purposes you pattern match on a type-indexed TypeRep from Type.Reflection. pattern FromSing and pattern TypeRep were recently added, not to be confused with the TypeRep type constructor so check to see if you have the latest version.

pattern STypeRep :: () => Typeable a => SType a
pattern STypeRep <- (stypeRep -> TypeRep)
--where STypeRep = stype typeRep

stypeRep :: SType a -> TypeRep a
stypeRep = \case
 SInteger -> typeRep
 SBoolean -> typeRep
 SByteStr -> typeRep

-- optional and partial actually
-- stype :: forall a. TypeRep a -> SType a
-- stype rep
--   | Just HRefl <- eqTypeRep rep (typeRep @Int)
--   = SInteger
--   | Just HRefl <- eqTypeRep rep (typeRep @Bool)
--   = SBoolean
--   | Just HRefl <- eqTypeRep rep (typeRep @ByteString)
--   = SByteStr
--   | let
--   = error "crash and burn"

The final form:

checkResult :: EType -> UntypedExp -> Maybe Result
checkResult (FromSing singType@STypeRep) = fmap (makeResult singType) . inferExpr