Allow building with mmorph-1.1.0 on GHC 8.0.1 and older

[RyanGlScott]

If you try to build ether-0.5.0.0 with mmorph-1.1.0 (which made MFunctor poly-kinded) on GHC 8.0.1 or older, you'll get this inscrutable error message:

[1 of 8] Compiling Ether.Internal   ( src/Ether/Internal.hs, dist/build/Ether/Internal.o )
[2 of 8] Compiling Ether.TaggedTrans ( src/Ether/TaggedTrans.hs, dist/build/Ether/TaggedTrans.o )

src/Ether/TaggedTrans.hs:36:48: error:
    • No instance for (MFunctor trans)
        arising from the 'deriving' clause of a data type declaration
      Possible fix:
        use a standalone 'deriving instance' declaration,
          so you can specify the instance context yourself
    • When deriving the instance for (MMonad (TaggedTrans tag trans))

This is a result of GHC Trac #11837, a bug which was fixed in GHC 8.0.2 (see https://github.com/Gabriel439/Haskell-MMorph-Library/issues/32). To work around this issue, I simply write out the MFunctor instance for TaggedTrans by hand.

[int-index]

Thank you!

Is the bug triggered if we use coerce the same way that GND-generated code does but specify the kinds?

[int-index]

I tried to test your fix using the following stack.yaml:

resolver: lts-7.23
packages: ['.']
extra-deps:
- transformers-lift-0.2.0.1
- mmorph-1.1.0

but the error is still there:

src/Ether/TaggedTrans.hs:36:38: error:
    • No instance for (MFunctor trans)
        arising from the 'deriving' clause of a data type declaration
      Possible fix:
        use a standalone 'deriving instance' declaration,
          so you can specify the instance context yourself
    • When deriving the instance for (MMonad (TaggedTrans tag trans))

Notice that the problem is with the MMonad instance.

[RyanGlScott]

Is the bug triggered if we use coerce the same way that GND-generated code does but specify the kinds?

I can't even get an implementation using coerce to typecheck, actually. If I try this:

instance MFunctor trans => MFunctor (TaggedTrans tag trans) where
    hoist :: forall m n b. Monad m => (forall a. m a -> n a)
          -> TaggedTrans tag trans m b -> TaggedTrans tag trans n b
    hoist = coerce hoistTrans
      where
        hoistTrans :: (forall a. m a -> n a) -> trans m b -> trans n b
        hoistTrans = hoist

Then GHC yells at me:

src/Ether/TaggedTrans.hs:184:13: error:
    • Cannot instantiate unification variable ‘b0’
      with a type involving foralls:
        (forall a. m a -> n a)
        -> TaggedTrans tag trans m b -> TaggedTrans tag trans n b
        GHC doesn't yet support impredicative polymorphism
    • In the expression: coerce hoistTrans
      In an equation for ‘hoist’:
          hoist
            = coerce hoistTrans
            where
                hoistTrans :: (forall a. m a -> n a) -> trans m b -> trans n b
                hoistTrans = hoist
      In the instance declaration for ‘MFunctor (TaggedTrans tag trans)’
    • Relevant bindings include
        hoistTrans :: (forall a. m a -> n a) -> trans m b -> trans n b
          (bound at src/Ether/TaggedTrans.hs:187:9)
        hoist :: (forall a. m a -> n a)
                 -> TaggedTrans tag trans m b -> TaggedTrans tag trans n b
          (bound at src/Ether/TaggedTrans.hs:184:5)

src/Ether/TaggedTrans.hs:184:20: error:
    • Cannot instantiate unification variable ‘a0’
      with a type involving foralls:
        (forall a. m a -> n a) -> trans m b -> trans n b
        GHC doesn't yet support impredicative polymorphism
    • In the first argument of ‘coerce’, namely ‘hoistTrans’
      In the expression: coerce hoistTrans
      In an equation for ‘hoist’:
          hoist
            = coerce hoistTrans
            where
                hoistTrans :: (forall a. m a -> n a) -> trans m b -> trans n b
                hoistTrans = hoist
    • Relevant bindings include
        hoistTrans :: (forall a. m a -> n a) -> trans m b -> trans n b
          (bound at src/Ether/TaggedTrans.hs:187:9)
        hoist :: (forall a. m a -> n a)
                 -> TaggedTrans tag trans m b -> TaggedTrans tag trans n b
          (bound at src/Ether/TaggedTrans.hs:184:5)

This is despite the fact that GeneralizedNewtypeDeriving is probably doing more-or-less the same thing under the hood... Weird.

[RyanGlScott]

but the error is still there:

src/Ether/TaggedTrans.hs:36:38: error:
    • No instance for (MFunctor trans)
        arising from the 'deriving' clause of a data type declaration
      Possible fix:
        use a standalone 'deriving instance' declaration,
          so you can specify the instance context yourself
    • When deriving the instance for (MMonad (TaggedTrans tag trans))

Notice that the problem is with the MMonad instance.

Rats, that's what I get for saying "of course it'll typecheck". I'll push a fix shortly.

[int-index]

This is despite the fact that GeneralizedNewtypeDeriving is probably doing more-or-less the same thing under the hood... Weird.

I tried to inline the code emitted by GND and after fixing the obvious errors (caused by pretty-printer) this is what I'm left with:

src/Ether/TaggedTrans.hs:189:7: error:
    • Illegal polymorphic type:
        forall (m_a9VF :: Type -> Type) (n_a9VG :: Type -> Type) b_a9VH.
        Monad m_a9VF =>
        (forall a_a9VI. m_a9VF a_a9VI -> n_a9VG a_a9VI)
        -> trans m_a9VF b_a9VH -> trans n_a9VG b_a9VH
      GHC doesn't yet support impredicative polymorphism
    • In the expression:
        coerce
          @(forall (m_a9VF :: Type -> Type)
                   (n_a9VG :: Type -> Type)
                   (b_a9VH :: Type).
            Monad m_a9VF =>
            (forall (a_a9VI :: Type). m_a9VF a_a9VI -> n_a9VG a_a9VI)
            -> trans m_a9VF b_a9VH -> trans n_a9VG b_a9VH)
          @(forall (m_a9VF :: Type -> Type)
                   (n_a9VG :: Type -> Type)
                   (b_a9VH :: Type).
            Monad m_a9VF =>
            (forall (a_a9VI :: Type). m_a9VF a_a9VI -> n_a9VG a_a9VI)
            -> TaggedTrans tag trans m_a9VF b_a9VH
               -> TaggedTrans tag trans n_a9VG b_a9VH)
          hoist
      In an equation for ‘hoist’:
          hoist
            = coerce
                @(forall (m_a9VF :: Type -> Type)
                         (n_a9VG :: Type -> Type)
                         (b_a9VH :: Type).
                  Monad m_a9VF =>
                  (forall (a_a9VI :: Type). m_a9VF a_a9VI -> n_a9VG a_a9VI)
                  -> trans m_a9VF b_a9VH -> trans n_a9VG b_a9VH)
                @(forall (m_a9VF :: Type -> Type)
                         (n_a9VG :: Type -> Type)
                         (b_a9VH :: Type).
                  Monad m_a9VF =>
                  (forall (a_a9VI :: Type). m_a9VF a_a9VI -> n_a9VG a_a9VI)
                  -> TaggedTrans tag trans m_a9VF b_a9VH
                     -> TaggedTrans tag trans n_a9VG b_a9VH)
                hoist
      In the instance declaration for ‘MFunctor (TaggedTrans tag trans)’

src/Ether/TaggedTrans.hs:217:7: error:
    • Illegal polymorphic type:
        forall (n_aa3N :: Type -> Type) (m_aa3O :: Type -> Type) b_aa3P.
        Monad n_aa3N =>
        (forall a_aa3Q. m_aa3O a_aa3Q -> trans n_aa3N a_aa3Q)
        -> trans m_aa3O b_aa3P -> trans n_aa3N b_aa3P
      GHC doesn't yet support impredicative polymorphism
    • In the expression:
        coerce
          @(forall (n_aa3N :: Type -> Type)
                   (m_aa3O :: Type -> Type)
                   (b_aa3P :: Type).
            Monad n_aa3N =>
            (forall (a_aa3Q :: Type). m_aa3O a_aa3Q -> trans n_aa3N a_aa3Q)
            -> trans m_aa3O b_aa3P -> trans n_aa3N b_aa3P)
          @(forall (n_aa3N :: Type -> Type)
                   (m_aa3O :: Type -> Type)
                   (b_aa3P :: Type).
            Monad n_aa3N =>
            (forall (a_aa3Q :: Type).
             m_aa3O a_aa3Q -> TaggedTrans tag trans n_aa3N a_aa3Q)
            -> TaggedTrans tag trans m_aa3O b_aa3P
               -> TaggedTrans tag trans n_aa3N b_aa3P)
          embed
      In an equation for ‘embed’:
          embed
            = coerce
                @(forall (n_aa3N :: Type -> Type)
                         (m_aa3O :: Type -> Type)
                         (b_aa3P :: Type).
                  Monad n_aa3N =>
                  (forall (a_aa3Q :: Type). m_aa3O a_aa3Q -> trans n_aa3N a_aa3Q)
                  -> trans m_aa3O b_aa3P -> trans n_aa3N b_aa3P)
                @(forall (n_aa3N :: Type -> Type)
                         (m_aa3O :: Type -> Type)
                         (b_aa3P :: Type).
                  Monad n_aa3N =>
                  (forall (a_aa3Q :: Type).
                   m_aa3O a_aa3Q -> TaggedTrans tag trans n_aa3N a_aa3Q)
                  -> TaggedTrans tag trans m_aa3O b_aa3P
                     -> TaggedTrans tag trans n_aa3N b_aa3P)
                embed
      In the instance declaration for ‘MMonad (TaggedTrans tag trans)’

Those errors go away as well if I enable -XImpredicativeTypes, but I'm hesitant to enable them because of how unreliable they are.

The fact that using coerce here forces me to enable -XImpredicativeTypes but using -XGeneralizedNewtypeDeriving doesn't - looks like a bug in itself.

Your fix is good, but I don't want to risk TaggedTrans not being zero-cost. Since the fix is already in GHC 8.0.2 and the coerce-based solution fails, I'm compelled to leave this PR open for now.

I will merge if:

• the generated Core is equally efficient, or
• the changes are behind CPP, or
• someone needs this fix badly.

[RyanGlScott]

Those errors go away as well if I enable -XImpredicativeTypes

Ah, that explains it. Internally, GHC enables ImpredicativeTypes when deriving things via GeneralizedNewtypeDeriving, so that's why you don't have to enable it unless you write out coerce explicitly.

In any case, I've put this workaround behind CPP.

[int-index]

GHC enables ImpredicativeTypes when deriving things via GeneralizedNewtypeDeriving

This is quite interesting. I thought that ImpredicativeTypes are considered broken, and now it turns out that GeneralizedNewtypeDeriving relies on them?

[RyanGlScott]

I suppose some background context would be useful here. It's well known that ImpredicativeTypes breaks when you bend it too far. In fact, Simon Peyton Jones has proposed to remove the extension entirely. The annoying thing is that currently, you need to enable ImpredicativeTypes to do something like this:

f x = id @(forall a. a->a) id @Int x

But, as SPJ notes in the above link, there's nothing about this which requires impredicativity, so visibly applying a rank-n type is perfectly safe to do. (He goes on to propose allowing such a thing without ImpredicativeTypes, which has yet to happen.) So for now, at least, visibly applying rank-n types falls within a very special, safe subset of ImpredicativeTypes that is known to work.