I can't get a GADT Dynamic based toy to work with parametric types

Question

Therefore, to help me understand some of the more advanced functions and concepts of Haskell / GHC, I decided to use a working version of dynamically typed data based on GADT and expand it to cover parametric types. (I apologize for the length of this example.)

{-# LANGUAGE GADTs #-} module Dyn ( Dynamic(..), toDynamic, fromDynamic ) where import Control.Applicative ---------------------------------------------------------------- ---------------------------------------------------------------- -- -- Equality proofs -- -- | The type of equality proofs. data Equal ab where Reflexivity :: Equal aa -- | Inductive case for parametric types Induction :: Equal ab -> Equal (fa) (fb) instance Show (Equal ab) where show Reflexivity = "Reflexivity" show (Induction proof) = "Induction (" ++ show proof ++ ")" ---------------------------------------------------------------- ---------------------------------------------------------------- -- -- Type representations -- -- | Type representations. If @x :: TypeRep a@ , then @ x@ is a singleton -- value that stands in for type @ a@. data TypeRep a where Integer :: TypeRep Integer Char :: TypeRep Char Maybe :: TypeRep a -> TypeRep (Maybe a) List :: TypeRep a -> TypeRep [a] -- | Typeclass for types that have a TypeRep class Representable a where typeRep :: TypeRep a instance Representable Integer where typeRep = Integer instance Representable Char where typeRep = Char instance Representable a => Representable (Maybe a) where typeRep = Maybe typeRep instance Representable a => Representable [a] where typeRep = List typeRep -- | Match two types and return @ Just@ an equality proof if they are -- equal, @ Nothing@ if they are not. matchTypes :: TypeRep a -> TypeRep b -> Maybe (Equal ab) matchTypes Integer Integer = Just Reflexivity matchTypes Char Char = Just Reflexivity matchTypes (List a) (List b) = Induction <$> (matchTypes ab) matchTypes (Maybe a) (Maybe b) = Induction <$> (matchTypes ab) matchTypes _ _ = Nothing instance Show (TypeRep a) where show Integer = "Integer" show Char = "Char" show (List a) = "[" ++ show a ++ "]" show (Maybe a) = "Maybe (" ++ show a ++ ")" ---------------------------------------------------------------- ---------------------------------------------------------------- -- -- Dynamic data -- data Dynamic where Dyn :: TypeRep a -> a -> Dynamic instance Show Dynamic where show (Dyn typ val) = "Dyn " ++ show typ -- | Inject a value of a @ Representable@ type into @ Dynamic@. toDynamic :: Representable a => a -> Dynamic toDynamic = Dyn typeRep -- | Cast a @ Dynamic@ into a @ Representable@ type. fromDynamic :: Representable a => Dynamic -> Maybe a fromDynamic = fromDynamic' typeRep fromDynamic' :: TypeRep a -> Dynamic -> Maybe a fromDynamic' target (Dyn source value) = case matchTypes source target of Just Reflexivity -> Just value Nothing -> Nothing -- The following pattern causes compilation to fail. Just (Induction _) -> Just value 

Compiling this, however, is not performed on the last line (line numbers do not match this example):

 ../src/Dyn.hs:105:34: Could not deduce (a2 ~ b) from the context (a1 ~ f a2, a ~ fb) bound by a pattern with constructor Induction :: forall ab (f :: * -> *). Equal ab -> Equal (fa) (fb), in a case alternative at ../src/Dyn.hs:105:13-23 `a2' is a rigid type variable bound by a pattern with constructor Induction :: forall ab (f :: * -> *). Equal ab -> Equal (fa) (fb), in a case alternative at ../src/Dyn.hs:105:13 `b' is a rigid type variable bound by a pattern with constructor Induction :: forall ab (f :: * -> *). Equal ab -> Equal (fa) (fb), in a case alternative at ../src/Dyn.hs:105:13 Expected type: a1 Actual type: a In the first argument of `Just', namely `value' In the expression: Just value In a case alternative: Just (Induction _) -> Just value 

The way I read this, the compiler cannot understand that in Inductive :: Equal ab -> Equal (fa) (fb) , a and b must be equal for invalid values. So I tried Inductive :: Equal aa -> Equal (fa) (fa) , but that also fails, in the definition of matchTypes :: TypeRep a -> TypeRep b -> Maybe (Equal ab) :

 ../src/Dyn.hs:66:60: Could not deduce (a2 ~ a1) from the context (a ~ [a1]) bound by a pattern with constructor List :: forall a. TypeRep a -> TypeRep [a], in an equation for `matchTypes' at ../src/Dyn.hs:66:13-18 or from (b ~ [a2]) bound by a pattern with constructor List :: forall a. TypeRep a -> TypeRep [a], in an equation for `matchTypes' at ../src/Dyn.hs:66:22-27 `a2' is a rigid type variable bound by a pattern with constructor List :: forall a. TypeRep a -> TypeRep [a], in an equation for `matchTypes' at ../src/Dyn.hs:66:22 `a1' is a rigid type variable bound by a pattern with constructor List :: forall a. TypeRep a -> TypeRep [a], in an equation for `matchTypes' at ../src/Dyn.hs:66:13 Expected type: TypeRep a1 Actual type: TypeRep a In the second argument of `matchTypes', namely `b' In the second argument of `(<$>)', namely `(matchTypes ab)' 

Changing the type of matchTypes :: TypeRep a -> TypeRep b -> Maybe (Equal ab) to create matchTypes :: TypeRep a -> TypeRep b -> Maybe (Equal aa) does not work (just read it as a sentence). Also there is no matchTypes :: TypeRep a -> TypeRep a -> Maybe (Equal aa) (another trivial sentence, and this, as I understand it, will require users fromDynamic' to know the a in the TypeRep a contained in the Dynamic`).

So I'm at a dead end. Any pointers on how to move forward here?

Answer 1

The problem is that the template template template loses equality information. If you code induction this way, you cannot write a (final) collection of patterns that covers all cases. The solution is to infer the induction from your data type into a specific value. The relevant changes are as follows:

 data Equal ab where Reflexivity :: Equal aa induction :: Equal ab -> Equal (fa) (fb) induction Reflexivity = Reflexivity matchTypes (List a) (List b) = induction <$> matchTypes ab matchTypes (Maybe a) (Maybe b) = induction <$> matchTypes ab fromDynamic' :: TypeRep a -> Dynamic -> Maybe a fromDynamic' target (Dyn source value) = case matchTypes source target of Just Reflexivity -> Just value Nothing -> Nothing 

Thus, the templates in fromDynamic' are comprehensive, but do not have any characters that lose information.