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

[Dmitriy Matrosov]

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?