Hi, Richard.

- Have you looked at https://hackage.haskell.org/package/base-4.16.0.0/docs/Data-Dynamic.html ? That may have the functionality you're looking for. It's quite a bit simpler than the construction you're building, but it might satisfy your eventual use-case.

Not yet. In fact, i don't have any particular use-case, i'm just reading "thinking with types" book and tried to experiment a little. But anyway, i'll look at this package, thanks!

- GHC does not distinguish between types and kinds, since GHC 8.0. Much literature about Haskell continues to make this distinction, including GHC's own error messages (at some implementation challenge, even). This is because, most of the time, programs don't cross the line between types and kinds, and this distinction can be helpful. However, your code does shuttle ideas back and forth across the line, and so the distinction is harmful. Bottom line here: treat types and kinds as synonyms. The design of Haskell does, internally.

So.. does this mean that there are only two "things" now: "something" and "type of something". And this "something" may be either value or type. And when "something" is type, it's type is what was previously called kind? And the exact same type variable may denote the type of both "something"-s (values and types) at the same time (i.e. in the one expression)?

- I think the crux of your question is why (Just t :: Maybe t) fails to type-check. We can see this in the type of Just: Just :: forall (a :: Type). a -> Maybe a. When we write `Just t` (for `t :: Type`), GHC sees `Just @Type t`, supplying the invisible instantiation for the `forall (a :: Type)` argument in Just's type. We can now see that `Just @Type t` will have type `Maybe Type`, just by substituting in Just's type. So saying `Just t :: Maybe t` will be rejected.

- On the other hand, `Nothing :: Maybe t` is fine. We have `Nothing :: forall (a :: Type). Maybe a`, and so `Nothing :: Maybe t` really means `Nothing @t :: Maybe t`, and all is well.

Thanks a lot, I think that I understand now. 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 worry that there is more in your email that I haven't answered here. If so, please write back!

Richard

On Dec 31, 2021, at 8:33 AM, Dmitriy Matrosov wrote:

...

- GHC does not distinguish between types and kinds, since GHC 8.0. Much literature about Haskell continues to make this distinction, including GHC's own error messages (at some implementation challenge, even). This is because, most of the time, programs don't cross the line between types and kinds, and this distinction can be helpful. However, your code does shuttle ideas back and forth across the line, and so the distinction is harmful. Bottom line here: treat types and kinds as synonyms. The design of Haskell does, internally.

So.. does this mean that there are only two "things" now: "something" and "type of something". And this "something" may be either value or type. And when "something" is type, it's type is what was previously called kind?

I would say Haskell has terms and types. It also has two relations: type-of-term and type-of-type. The type of a term (using the type-of-term relation) connects a term to a type. The type of a type (using the type-of-type relation) connects a type with another type. Some would say that the type-of-type relation connects a type with a kind, but "kind" is really just a synonym for "type". The design of Haskell has arranged that, for data constructors, the type-of-term relation and the type-of-type relation coincide. That is, the phrase `Just :: forall a. a -> Maybe a` is true both when `Just` is a term (and we're talking about the type-of-term relation) and when `Just` is a type (and we're talking about the type-of-type relation).

And the exact same type variable may denote the type of both "something"-s (values and types) at the same time (i.e. in the one expression)?

I think so -- I'm not sure I understand your phrasing fully. Because types and kinds are the same, one type variable may be used both in a type-of-a-term and in the type-of-a-type.

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. I hope this helps! Richard

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?

On 1/26/22 10:38 PM, Richard Eisenberg wrote:

I was at a conference last week and didn't have time to respond... but now that I return to this, I still don't really understand what your question is. Sorry!

I think this will help: Why invoke GHC.Types.Any at all? What are you hoping to accomplish with GHC.Types.Any?

Well, that's more of a theoretical question. As i wrote earlier, i've fixed this example (by using type-class definition similar to IsLabel and without GHC.Types.Any). But anyway, i try to explain shorter. I've had the following code, which defines head function for using on list of existentials and coercing the head back to original type according to type-level list:

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

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

headAny :: forall ts . FromTypeMaybe (MaybeHead ts) => Proxy ts -> [AnyData] -> Maybe (ToType (MaybeHead ts)) headAny _ [] = Nothing headAny _ (x : xs) = fromTypeMaybe unAny (Proxy @(MaybeHead ts)) x

This code works, when type-level list specified explicitly, like *Main> headAny @('[Int, Bool]) Proxy [AnyData 1, AnyData True] Just 1 but when i use 'Tail' function on type-level list with 1 element, it does not work: *Main> headAny @(Tail '[Bool]) Proxy [AnyData 1, AnyData True] <interactive>:22:1: error: • No instance for (Show *) arising from a use of ‘print’ • In a stmt of an interactive GHCi command: print it Though on list with many elements and with empty list everything works: *Main> headAny @(Tail '[]) Proxy [AnyData 1, AnyData True] Nothing When i've tried to understand why, i've noticed some similarities between working empty list case and non-working 1-element case: both these cases work through 'Nothing instance of 'FromTypeMaybe' type class, but type variable t is defined differently: *Main> :k! MaybeHead (Tail '[]) MaybeHead (Tail '[]) :: Maybe t = 'Nothing *Main> :k! MaybeHead (Tail '[Bool]) MaybeHead (Tail '[Bool]) :: Maybe * = 'Nothing So, with empty list type variable t remains unbound, but with 1-element list it is bound to Type. And then (ToType 'Nothing) is defined accordingly: *Main> :k! ToType (MaybeHead (Tail '[])) ToType (MaybeHead (Tail '[])) :: * = GHC.Types.Any *Main> :k! ToType (MaybeHead (Tail '[Bool])) ToType (MaybeHead (Tail '[Bool])) :: * = * And, no surprise, that there's no (Show Type) instance: *Main> show $ headAny @(Tail '[Bool]) Proxy [AnyData 1, AnyData True] <interactive>:38:1: error: • No instance for (Show *) arising from a use of ‘show’ Until that moment, i understand everything (i think). But then ghc somehow manages to find Show instance for GHC.Types.Any (or may be not, but how does it print result for empty list then?): *Main> show $ headAny @(Tail '[]) Proxy [AnyData 1, AnyData True] "Nothing" And that's the first thing i don't understand: there's should be no Show instance, but still.. Then i thought, that by defining (ToType 'Nothing) to be GHC.Types.Any instead of t: instance forall (t :: Type). FromTypeMaybe ('Nothing @t) where type ToType 'Nothing = GHC.Types.Any fromTypeMaybe f _ x = Nothing i may fix 1-element case. Type evaluation looked promising: *Main> :k! (MaybeHead (Tail '[])) (MaybeHead (Tail '[])) :: Maybe t = 'Nothing *Main> :k! ToType (MaybeHead (Tail '[])) ToType (MaybeHead (Tail '[])) :: * = GHC.Types.Any but it does not work: *Main> show $ headAny @(Tail '[Bool]) Proxy [AnyData 1, AnyData True] <interactive>:44:1: error: • No instance for (Show GHC.Types.Any) arising from a use of ‘show’ *Main> show $ headAny @(Tail '[]) Proxy [AnyData 1, AnyData True] <interactive>:45:1: error: • No instance for (Show GHC.Types.Any) arising from a use of ‘show’ And that's the second thing i don't understand: why it does not work, when i explicitly define type to be equal to GHC.Types.Any? Thanks. PS. I've read "Any types" notes in GHC.Builtin.Types, but apart from that ghc uses 'GHC.Types.Any' internally to unify (?) unconstrained types, i don't understand much, sorry.

...

On Jan 18, 2022, at 8:10 AM, Dmitriy Matrosov wrote:

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? _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

On 1/28/22 11:48 PM, Richard Eisenberg wrote:

...

On Jan 27, 2022, at 10:25 AM, Dmitriy Matrosov wrote:

but when i use 'Tail' function on type-level list with 1 element, it does not work:

*Main> headAny @(Tail '[Bool]) Proxy [AnyData 1, AnyData True]

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

This is all about defaulting.

The key question: what is the type of the expression you are typing?

- With `headAny @(Tail '[Bool]) Proxy [AnyData 1, AnyData True]`, the type is `Maybe (ToType (MaybeHead (Tail '[Bool])))`. We see that `Tail '[Bool] :: [Type]` reduces to `'[] :: [Type]`. Then, `MaybeHead (Tail '[Bool]) :: Maybe Type` reduces to `Nothing :: Maybe Type`. And finally `ToType (Nothing :: Maybe Type)` reduces to `Type`, meaning that your expression has type `Maybe Type`. Because GHC won't print out something unless it has a Show instance, it bleats, saying there is no Show instance for `Maybe Type`.

- Now, consider `headAny @(Tail '[]) Proxy [AnyData 1, AnyData True]`. The result type is `Maybe (ToType (MaybeHead (Tail '[])))`. The point of interest here is: what is the type of `Tail '[]`? It's a list, but the element type is unconstrained. So GHC invents a fresh variable `t`. Following a similar sequence as above, we end up with assigning the expression the type `Maybe t`. At this point, GHC wants to print something of type `Maybe t` but doesn't know what `t` is. It tries `()` as a substitution for `t`. (https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/ghci.html?hi...) That works, and the "Nothing" is printed.

In other circumstances -- where there is no Show constraint around, for example -- GHC will take an unknown type variable (like t) and default it to GHC.Types.Any. So, you're right that there is no `Show Any` constraint, but GHC doesn't need one, because of its clever (and confusing!) approach to defaulting.

Does this help? Richard

Yes, thanks! I understand now.