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

[Viktor Dukhovni]

On Fri, Dec 31, 2021 at 04:33:28PM +0300, Dmitriy Matrosov wrote:

> 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
>    |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

The error is a technicality, it goes away if you give `Nothing` an
explicit type (kind):

    instance forall (t :: Type). FromTypeMaybe ('Nothing :: Maybe t) where
      type ToType ('Nothing :: Maybe t) = t
      fromTypeMaybe f _ x = Nothing

-- 
    Viktor.