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

[Dmitriy Matrosov]

On 1/28/22 11:48 PM, Richard Eisenberg wrote:
> 
>> 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
> 

Yes, thanks! I understand now.