Issue with polymorphic associated types

Hi, I have a class defined like such:

class Failable c where
  type Failure c :: *
  initWithFailure :: Failure c -> c

And I want to define it for Maybe like this:

instance Failable (Maybe c) where
  initWithFailure :: forall a . a -> forall e . Maybe e
  initWithFailure _ = Nothing

If I compile this as is, the ghc will complain that the Failure is not defined, but I apparently cannot specify Failure as

type Failure (Maybe _) = forall a . a

Why does it result in error? Is there any intention to rectify this behaviour?

For the record, the error is:

<interactive>:6:40: error:
    * Illegal polymorphic type: forall a. a
    * In the type instance declaration for `Failure'
      In the instance declaration for `Failable (Maybe c)'

I don’t think there is a way to fix that error. It just seems to be a limitation of how associated types work for type classes. But I don’t know exactly why this restriction is in place.

But even if it did work, then it probably wouldn’t do what you expect. You’d get:

initWithFailure :: (forall a. a) -> Maybe c

The type forall a. a means that the value must be able to be of any type, which is only true for undefined. No real value can have that type.

You probably wanted the type:

initWithFailure :: forall a. (a -> Maybe c)

Which means that the function can accept any type as input.

I don’t think there is a simple way to get that to work. I can only think of this now:

import Data.Kind (Constraint)

class Failable c where
  type Failure c a :: Constraint
  initWithFailure :: Failure c a => a -> Maybe c

instance Failable c where
  type Failure (Maybe _) _ = ()
  initWithFailure :: a -> Maybe c
  initWithFailure _ = Nothing
1 Like

I’m not sure what you are trying to do. Using my best guess something like this should work:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}

class Failable f a where
  initWithFailure :: f -> a

instance Failable f (Maybe a) where
  initWithFailure _ = Nothing

working meaning that this will get you Nothing: initWithFailure "whatever" :: Maybe Int

It does work.

oh :: forall a . a -> forall a . Maybe a
oh _ = Nothing

_ :: Maybe () = oh ()

This is accepted without any issues, I just checked.


Yeah, thanks for the shot, but really need this to be polytype (or whatever this called). The Failure example I gave is rather for simplicity, because I have a case where I cannot opt into multiparam tc.

class (Transient (Exodus ctx)) => Transient ctx where
   type Focus ctx :: *
   type Exodus ctx :: *
   transfer :: ctx -> (Focus ctx -> Exodus ctx) -> Exodus ctx

Then if I were to define an instance for Maybe i’d need infinite amoun of refinement if I were to do it with Transient i o


Any of you know if this to be ever streamline in foreseeable time?

This is accepted without any issues, I just checked.

Yes, but that is not what you would get. You would get this:

oh :: (forall a . a) -> forall a . Maybe a

Because you would have

type instance Failure (Maybe _) = forall a. a

Substituting that in initWithFailure :: (Failure (Maybe c)) -> Maybe c gets you:

initWithFailure :: (forall a. a) -> Maybe c

Similar to how you can define f = \x -> x and substitute it into f True to get (\x -> x) True and not \x -> x True.

2 Likes

Ah, you’re right. But then, is there a way to specify that I need a constrained type that is ‘existential’ (is this right word for it?); what people reach for in such cases?

How annoying would it be to just do:

instance Failable (Maybe c) where
  type Failure (Maybe _) = ()
  initWithFailure _ = Nothing
1 Like