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

[Richard Eisenberg]

Thanks. Now I understand much better.

> On Jan 27, 2022, at 10:25 AM, Dmitriy Matrosov <sgf.dma at gmail.com> 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?highlight=extendeddefaultrules#type-defaulting-in-ghci) 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