James M <jmartin@eecs.berkeley.edu> writes:

> This is easily testable.
>
> deriving instance Typeable Entry
> deriving instance Typeable FileKind
> deriving instance Typeable 'FOLDER
> deriving instance Typeable 'FILE
>
> convertBack :: SomeEntry -> Either (Entry FILE) (Entry FOLDER)
> convertBack (SomeEntry x)
>     | typeOf x == typeOf (Folder "" "") = Right x
>     | otherwise = Left x


If the goal is just to write the `convertBack' function with the type
signature above you don't need Typeable. If you enable the GADT
extension you can just pattern match on the Entry that is stored in the
SomeEntry, even though they have different types: i.e.

convertBack :: SomeEntry -> Either (Entry FILE) (Entry FOLDER)
convertBack (SomeEntry f@(File _ _ _)) = Left f
                                         -- By pattern matching on f we
                                         -- can convince the compiler
                                         -- that f  is of type Entry FILE
convertBack (SomeEntry d@(Folder _ _)) = Right d

Similarly we can write a function

convertAsFile :: SomeEntry -> Entry FILE
convertAsFile (SomeEntry f@(File _ _ _)) = f
convertAsFile (SomeEntry d) = error "We cannot convert from a Entry FOLDER"

however there is no way of making that function total (i.e. in the
second case there is no proper way of constructing an Entry FILE from an
Entry FOLDER)

Because you can (locally) recover the type by pattern matching on a GADT
I prefer to use GADTs to model existential types rather than using the
ExistentialTypes extension.

--

- Frank