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