[Haskell-cafe] Coercing existential according to type-level Maybe (re-post from h-beginners)

[Dmitriy Matrosov]

(as suggested, i'm re-asking here)

Hi.

I've tried to write a function to coerce existential value according to type
stored in type-level 'Maybe' (i.e. 'Just or 'Nothing).

> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE RankNTypes #-}
> {-# LANGUAGE KindSignatures #-}
> {-# LANGUAGE PolyKinds #-}
> {-# LANGUAGE TypeFamilies #-}
> {-# LANGUAGE GADTs #-}
>
> import Data.Kind
> import Data.Proxy
> import Unsafe.Coerce
>
> class FromTypeMaybe k where
>     type ToType k
>     fromTypeMaybe :: (a -> ToType k) -> Proxy k -> a -> Maybe (ToType k)
>
> --instance forall (t :: Type). FromTypeMaybe ('Nothing :: Maybe t) where
> instance forall (t :: Type). FromTypeMaybe ('Nothing @t) where
>     type ToType 'Nothing = t
>     fromTypeMaybe f _ x = Nothing
>
> instance forall (t :: Type). FromTypeMaybe ('Just t :: Maybe Type) where
>     type ToType ('Just t) = t
>     fromTypeMaybe f _ x = Just (f x)
>
> data Any where
>     Any :: a -> Any
>
> unAny :: Any -> t
> unAny (Any x) = unsafeCoerce x

This works as far as i can see

    *Main> fromTypeMaybe unAny (Proxy @('Just Int)) (Any 3)
    Just 3
    *Main> fromTypeMaybe unAny (Proxy @'Nothing) undefined
    Nothing

but i don't understand how 'Nothing instance works:

                   type   kind                                  kind?
                    vvv  vvvvvv                                  vvv
    instance forall (t :: Type). FromTypeMaybe ('Nothing :: Maybe t) where
         type ToType 'Nothing = t
                               ^^^
                               type

(in case alignment breaks: variable 't' in forall is type-variable with kind
'Type', but in "Maybe t" in instance head it's used as kind-variable. And then
in associated type-family the same variable 't' is used as type-variable
again).

If i try to write "'Nothing"'s kind as 'Maybe Type' (in the same manner as
'Just has)

    instance forall (t :: Type). FromTypeMaybe ('Nothing :: Maybe Type) where

i get an error:

    1.lhs:21:3: error:
        • Type variable ‘t’ is mentioned in the RHS,
            but not bound on the LHS of the family instance
        • In the type instance declaration for ‘ToType’
          In the instance declaration for
            ‘FromTypeMaybe ('Nothing :: Maybe Type)’
       |
    21 | > instance forall (t :: Type). FromTypeMaybe ('Nothing ::
Maybe Type) where
       |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

Well, i'm not sure, that understand why 'forall' in instance head may not be
used as family's LHS, but.. that's another question.  On the other
hand, if i try
to write 'Just instance using type-variable 't' as kind-variable (in the same
manner as 'Nothing has):

    instance forall (t :: Type). FromTypeMaybe ('Just t :: Maybe t) where

i get an error too:

    1.lhs:25:47: error:
        • Expected kind ‘Maybe t’, but ‘'Just t’ has kind ‘Maybe *’
        • In the first argument of ‘FromTypeMaybe’, namely
            ‘('Just t :: Maybe t)’
          In the instance declaration for
            ‘FromTypeMaybe ('Just t :: Maybe t)’
       |
    25 | > instance forall (t :: Type). FromTypeMaybe ('Just t :: Maybe t) where

Well, that's also probably expected, because though i've declared
type-variable 't' with kind 'Type' in forall, due to 'DataKinds' extension
type 't' is also promoted to kind 't' and, thus, by using ('Just t :: Maybe t)
i say, that ('Just t) should have kind 'Maybe t', not 'Maybe Type', which it
really has.

But if that's so, how working 'Nothing instance

    instance forall (t :: Type). FromTypeMaybe ('Nothing :: Maybe t) where

may work at all? It has the same problem as 'Just instance above:
type-variable 't' is promoted to kind 't' and 'Nothing will have kind 'Maybe
t' instead of 'Maybe Type' ?