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' ?
