Haskell: proving with Typeable that `exists t. a ~ D t`

Question

I have

data D t = ...
data SomeStuff = forall a (Typeable a, ...) => SomeStuff a

and at some point I get a SomeStuff whose internal a I'd like to try and cast to D t (where t can by any type, I'm only interested in the D part). Something which (in pseudo-Haskell) would look like:

case someStuff of
  SomeStuff (_ :: a) -> case eqT :: Maybe (a :~: (exists t. D t)) of
    Just Refl -> -- proven that `exists t. a ~ D t`
    Nothing -> -- nothing to do here

I've been fiddling around with Data.Type.Equality and Type.Reflection (like App etc) and I can't get it to work. Anyone has a way to do that?

Answer 1

Testing whether the type is of the form D _ can be achieved exploiting Type.Reflection, as follows.

We start from giving some concrete definitions modeled on your example, so that we can test our code later on.

{-# LANGUAGE GADTs, RankNTypes, ScopedTypeVariables, TypeOperators, TypeApplications #-}
{-# OPTIONS -Wall #-}

import Type.Reflection

data D t = D1 | D2  -- whatever
data SomeStuff = forall a. (Typeable a, Show a) => SomeStuff a

Then, we test for D _ as follows:

foo :: SomeStuff -> (forall t. D t -> String) -> String
foo (SomeStuff (x :: a)) f = case typeRep @a of
   App d _ | Just HRefl <- eqTypeRep (typeRep @D) d -> f x
   _ -> "the SomeStuff argument does not contain a value of type D t for any t"

Above, we take as arguments both the SomeStuff value and a polymorphic function f. The latter requires an argument of the form D _ and is used here only to show that our approach actually works -- you can remove the f argument if you don't need that.

After that, we take takeRep @a which models the (reflected) type representation of our unknown type a. We check whether that matches with the pattern App d _, i.e. whether type a is an application of d to something we don't care _. If so, we check whether d is indeed the (reflected representation of) our D type constructor. Matching the result of eqTypeRepl against Just HRefl makes GHC assume a ~ D t for some fresh type variable t, which is what we want. After that, we can call f x confirming GHC inferred the wanted type.

As an alternative, we can exploit view patterns to make our code more compact, without sacrificing the readability too much:

foo :: SomeStuff -> (forall t. D t -> String) -> String
foo (SomeStuff (x :: a)) f = case typeRep @a of
   App (eqTypeRep (typeRep @D) -> Just HRefl) _ -> f x
   _ -> "the SomeStuff argument does not contain a value of type D t for any t"