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.