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

[Richard Eisenberg]

> On Dec 31, 2021, at 8:33 AM, Dmitriy Matrosov <sgf.dma at gmail.com> 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