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

[Dmitriy Matrosov]

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