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

[Dmitriy Matrosov]

On 1/3/22 5:26 PM, Richard Eisenberg wrote:
> 
>>   And does the error:
>>
>> coerce-existential-with-type-level-maybe.lhs:22: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 @Type)’
>>    |
>> 22 | > instance forall (t :: Type). FromTypeMaybe ('Nothing @Type) where
>>    |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
>>
>> when i try to apply 'Nothing to @Type instead of @t occurs, because
>> full form of associated type family is
>>
>>      type ToType ('Nothing @Type) = t
>>
>> and variable 't' becomes unbound?
> 
> I wouldn't quite say t is unbound there -- it refers to the t in the instance head. What's more troublesome is that, when GHC is trying to reduce `ToType (Nothing @Type)`, it has no way of knowing what `t` is. This is why GHC requires that all variables mentioned in the RHS of an associated type equation are also mentioned on the left.
> 

Hi, Richard.

I thought, that my 'FromTypeMaybe' works, but it turns out not always.

So, to recap:

> {-# 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

I think, that understand the problem, but yet don't know how to fix it.

If i evaluate types, i get

for 2-elements list

     *Main> :k! Tail '[Bool, Int]
     Tail '[Bool, Int] :: [*]
     = '[Int]
     *Main> :k! MaybeHead (Tail '[Bool, Int])
     MaybeHead (Tail '[Bool, Int]) :: Maybe *
     = 'Just Int
     *Main> :k! ToType (MaybeHead (Tail '[Bool, Int]))
     ToType (MaybeHead (Tail '[Bool, Int])) :: *
     = Int

for 1-element list

     *Main> :k! Tail '[Bool]
     Tail '[Bool] :: [*]
     = '[]
     *Main> :k! MaybeHead (Tail '[Bool])
     MaybeHead (Tail '[Bool]) :: Maybe *
     = 'Nothing
     *Main> :k! ToType (MaybeHead (Tail '[Bool]))
     ToType (MaybeHead (Tail '[Bool])) :: *
     = *

and for empty list

     *Main> :k! Tail '[]
     Tail '[] :: [t]
     = '[]
     *Main> :k! MaybeHead (Tail '[])
     MaybeHead (Tail '[]) :: Maybe t
     = 'Nothing
     *Main> :k! ToType (MaybeHead (Tail '[]))
     ToType (MaybeHead (Tail '[])) :: *
     = GHC.Types.Any

Thus, for 1-element case in type-family 'Tail' type-of-type variable t gets
instantiated to '*', because there is one element in list ('Bool' in the
example) and its type (kind) is '*'. Then this type '*' goes through
'MaybeHead' and i get ('Nothing :: Maybe *), and type variable t in
'FromTypeMaybe' instance head also gets instantiated to '*'. And then it's
just substituted in 'ToType' RHS. And i end up looking for (Show *) instance.

In the empty list case, though, type-of-type variable 't' from 'Tail' remains
as type variable till the end. But then (for some reason) GHC replaces it with
'GHC.Types.Any' and (yet more strangely) manages to find 'Show' instances for
'GHC.Types.Any'.

When i've tried to check may understanding and changed 'Tail' type to

     type Tail :: [*] -> [*]

the empty list case behaves like the 1-element case before:

     *Main> :k! ToType (MaybeHead (Tail '[]))
     ToType (MaybeHead (Tail '[])) :: *
     = *

     *Main> :t headAny (Proxy @(Tail '[])) $  insertAny 1 $ insertAny True []
     headAny (Proxy @(Tail '[])) $  insertAny 1 $ insertAny True []
       :: Maybe *
     *Main> headAny (Proxy @(Tail '[])) $  insertAny 1 $ insertAny True []

     <interactive>:309:1: error:
         • No instance for (Show *) arising from a use of ‘print’
         • In a stmt of an interactive GHCi command: print it

and (not surprisingly) does not work.

On the other hand, if i explicitly assign 'GHC.Types.Any' as 'ToType k' RHS in
'Nothing instance

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

then the 1-element case seems to become the same as the (working) empty list
case from before

     *Main> :k! ToType (MaybeHead (Tail '[Bool]))
     ToType (MaybeHead (Tail '[Bool])) :: *
     = GHC.Types.Any
     *Main> :k! ToType (MaybeHead (Tail '[]))
     ToType (MaybeHead (Tail '[])) :: *
     = GHC.Types.Any


but GHC still can't find 'Show GHC.Types.Any' instance:

     *Main> headAny (Proxy @(Tail '[Bool])) $  insertAny 1 $ insertAny True []
     <interactive>:327:1: error:
         • No instance for (Show GHC.Types.Any)
             arising from a use of ‘print’
           There are instances for similar types:
             instance Show base-4.14.3.0:Data.Semigroup.Internal.Any
               -- Defined in ‘base-4.14.3.0:Data.Semigroup.Internal’
         • In a stmt of an interactive GHCi command: print it

     *Main> headAny (Proxy @(Tail '[])) $  insertAny 1 $ insertAny True []
     <interactive>:328:1: error:
         • No instance for (Show GHC.Types.Any)
             arising from a use of ‘print’
           There are instances for similar types:
             instance Show base-4.14.3.0:Data.Semigroup.Internal.Any
               -- Defined in ‘base-4.14.3.0:Data.Semigroup.Internal’
         • In a stmt of an interactive GHCi command: print it

Well, probably, the problem is that i don't understand what is 'GHC.Types.Any'
and how GHC finds 'Show' instance for it ('Any types' notes in
GHC.Builtin.Types does not explain much; probably, i need to read the book
further instead..)

And besides i don't see any way of fixing my (FromTypeMaybe 'Nothing)
instance.

Thanks.