New subject: Coercing existential according to type-level Maybe

30 Dec 2021

      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
    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 probably ok.  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' ?

Coercing existential according to type-level Maybe

Dmitriy Matrosov

Kim-Ee Yeoh

tags

participants (2)