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

18 Jan 2022

      On 1/17/22 6:49 PM, Dmitriy Matrosov wrote:
...
...
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts #-}
import Data.Kind
import Data.Proxy
import Unsafe.Coerce
import qualified GHC.Types as GHC.Types
class FromTypeMaybe k where
    type ToType k
    fromTypeMaybe :: (a -> ToType k) -> Proxy k -> a -> Maybe (ToType k)
...
instance forall (t :: Type). FromTypeMaybe ('Nothing @t) where
    --type ToType 'Nothing = GHC.Types.Any
    type ToType 'Nothing = t
    fromTypeMaybe f _ x = Nothing
...
instance forall (t :: Type). FromTypeMaybe ('Just @Type t) where
    type ToType ('Just t) = t
    fromTypeMaybe f _ x = Just (f x)
then i've written a little more:
...
type MaybeHead :: [t] -> Maybe t
type family MaybeHead ts where
    MaybeHead '[] = 'Nothing
    MaybeHead (x ': xs) = 'Just x
type Tail:: [t] -> [t]
type family Tail ts where
    Tail '[] = '[]
    Tail (x ': xs) = xs
data AnyData where
    AnyData :: a -> AnyData
unAny :: AnyData -> t
unAny (AnyData x) = unsafeCoerce x
insertAny :: t -> [AnyData] -> [AnyData]
insertAny x zs = AnyData x : zs
headAny
    :: forall ts
    . FromTypeMaybe (MaybeHead ts)
    => Proxy ts -> [AnyData] -> Maybe (ToType (MaybeHead ts))
headAny _ [] = Nothing
headAny _ (x : xs) = fromTypeMaybe unAny (Proxy @(MaybeHead ts)) x
And now it works, when type-level list is explicitly specified, like:
    *Main> headAny (Proxy @'[]) $  insertAny 1 $ insertAny True []
     Nothing
     *Main> headAny (Proxy @'[Int]) $  insertAny 1 $ insertAny True []
     Just 1
     *Main> headAny (Proxy @'[Int, Bool]) $  insertAny 1 $ insertAny True []
     Just 1
but if i use 'Tail' type-function first, it works only in two cases:
for list with 2 or more elements
    *Main> :t headAny (Proxy @(Tail '[Bool, Int])) $  insertAny 1 $ insertAny True []
     headAny (Proxy @(Tail '[Bool, Int])) $  insertAny 1 $ insertAny True []
       :: Maybe Int
     *Main> headAny (Proxy @(Tail '[Bool, Int])) $  insertAny 1 $ insertAny True []
     Just 1
and empty list
    *Main> :t headAny (Proxy @(Tail '[])) $  insertAny 1 $ insertAny True []
     headAny (Proxy @(Tail '[])) $  insertAny 1 $ insertAny True []
       :: Maybe t
     *Main> headAny (Proxy @(Tail '[])) $  insertAny 1 $ insertAny True []
     Nothing
But for list with 1 element it does not work
    *Main> :t headAny (Proxy @(Tail '[Bool])) $  insertAny 1 $ insertAny True []
     headAny (Proxy @(Tail '[Bool])) $  insertAny 1 $ insertAny True []
       :: Maybe *
     *Main> headAny (Proxy @(Tail '[Bool])) $  insertAny 1 $ insertAny True []
    <interactive>:246:1: error:
         • No instance for (Show *) arising from a use of ‘print’
         • In a stmt of an interactive GHCi command: print it
.....
And besides i don't see any way of fixing my (FromTypeMaybe 'Nothing)
instance.
I think, i've fixed everything. Eventually, it was very simple.
...
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
import Data.Kind
import Data.Proxy
import Unsafe.Coerce
class FromTypeMaybe2 k t where
    fromTypeMaybe2 :: (a -> t) -> Proxy k -> a -> Maybe t
instance FromTypeMaybe2 'Nothing t where
    fromTypeMaybe2 f _ _ = Nothing
instance (t ~ t') => FromTypeMaybe2 ('Just t) t' where
    fromTypeMaybe2 f _ x = Just (f x)
headAny2
    :: forall t ts
    . FromTypeMaybe2 (MaybeHead ts) t
    => Proxy ts -> [AnyData] -> Maybe t
headAny2 _ [] = Nothing
headAny2 _ (x : xs) = fromTypeMaybe2 unAny (Proxy @(MaybeHead ts)) x
type MaybeHead :: [t] -> Maybe t
type family MaybeHead ts where
    MaybeHead '[] = 'Nothing
    MaybeHead (x ': xs) = 'Just x
type Tail:: [t] -> [t]
type family Tail ts where
    Tail '[] = '[]
    Tail (x ': xs) = xs
data AnyData where
    AnyData :: a -> AnyData
unAny :: AnyData -> t
unAny (AnyData x) = unsafeCoerce x
And now everything works:

     *Main> headAny2 (Proxy @'[]) $ [AnyData 1, AnyData True]
     Nothing
     *Main> headAny2 (Proxy @'[Int]) $ [AnyData 1, AnyData True]
     Just 1
     *Main> headAny2 (Proxy @'[Int, Bool]) $ [AnyData 1, AnyData True]
     Just 1

and

     *Main> headAny2 (Proxy @(Tail '[Bool, Int])) $ [AnyData 1, AnyData True]
     Just 1
     *Main> headAny2 (Proxy @(Tail '[Bool])) $ [AnyData 1, AnyData True]
     Nothing
     *Main> headAny2 (Proxy @(Tail '[])) $ [AnyData 1, AnyData True]
     Nothing

The only question, that remains is why defining 'Nothing resulting type to be
'GHC.Types.Any' in previous implementation

     instance forall (t :: Type). FromTypeMaybe ('Nothing @t) where
         type ToType 'Nothing = GHC.Types.Any

does not fix it?