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

The error I get is this:

    Couldn't match type ‘k’ with ‘'FOLDER’

      ‘k’ is a rigid type variable bound by

          a pattern with constructor

            SomeEntry :: forall (k :: FileKind). Entry k -> SomeEntry,

          in an equation for ‘convertBack’

          at cafe2.hs:24:14

    Expected type: Entry 'FOLDER

      Actual type: Entry k

    Relevant bindings include x :: Entry k (bound at cafe2.hs:24:24)

    In the first argument of ‘Right’, namely ‘x’

    In the expression: Right x

James

On Wed, Nov 12, 2014 at 11:29 PM, Bardur Arantsson <spam@scientician.net> wrote:

On 2014-11-13 08:10, James M wrote:
> I didn't explain Frank's case, only the one I constructed.
>
> convertBack :: SomeEntry -> Either (FsEntry FILE) (FsEntry FOLDER)
>
> For this function to work, we would need some way to inspect the type as a
> value, and this can only generally be done with dependent types.
>
> convertBack :: SomeEntry -> FsEntry k
>
> This case is technically possible to do statically, but not very useful
> because we have no idea what the actual type is. Therefore, we could only
> use it on things that work for all FsEntry and not just a subset.
>
> We could ask for what 'k' is in the type system and perform the necessary
> computation in the type system. However, this is complicated, and Haskell
> currently only has very limited support for moving between values and
> types. You can look at GHC.TypeLits for an example of this.

Maybe I'm missing something, but wouldn't adding a Typeable constraint
on the existential give you the option of casting back? AFAICT that
should be sufficient since the FileKind is closed and you can thus just
attempt both conversions and see which one succeeds.

Regards,

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe