CODEWITHSUNDEEP
haskelldependent-typetype-families
whitehead1415
whitehead1415

Reputation: 435

How to validate type family after storing it in json?

The following code won't compile and gives the error of

Couldn't match type ‘c1’ with ‘c’ ‘c1’ is a rigid type variable bound by a pattern with constructor: SomeReq :: forall c. Conn c => Req c -> SomeReq, in an equation for ‘run’

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ExistentialQuantification #-}

module Main where

import qualified Data.Text as T

class Conn c where
  data Auth c :: *
  data Env c :: *
  data Req c :: *

  getEnv :: Auth c -> IO (Env c)
  runReq :: Env c -> Req c -> IO String

data SomeAuth = forall c. (Conn c) => SomeAuth (Auth c)
data SomeReq = forall c. (Conn c) => SomeReq (Auth c)

run :: SomeAuth -> SomeReq -> IO String
run (SomeAuth auth) (SomeReq req) = do
  env <- getEnv auth
  runReq env req

main :: IO ()
main = return ()

The reason for the existentials is that I need to store these data types in json. (Auth c) and (Req c) are always stored seperatly, but are always used together.

I'm assuming that the only possible way to make this work is to have some kind of runtime check to validate that these types match up. I'm not sure how to do that though.

Upvotes: 1

Views: 89

Answers (1)

dfeuer
dfeuer

Reputation: 48611

Given a SomeAuth and a SomeReq, you have no way to find out whether the types they wrap are the same. If there are finitely many possibilities (a finite "universe"), then you can use a GADT to tag them:

data CTag c where
  C1T :: CTag C1
  C2T :: CTag C2
  ...

sticking a CTag in SomeAuth and one in SomeReq and pattern matching.

If c could be any old thing, your best bet is to use Data.Typeable, adding a Typeable constraint to the SomeAuth and SomeReq constructors. Once you open them both, you'll be able to find out if the types match, and if so get evidence of it.

Upvotes: 2

Related Questions