#8631 closed bug (fixed)

Need ImpredicativeTypes for GeneralizedNewtypeDeriving?

Reported by: goldfire Owned by:
Priority: normal Milestone: 7.8.1
Component: Compiler Version: 7.8.1-rc1
Keywords: Cc: mail@…, sweirich@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: deriving/should_compile/T8631
Blocked By: Blocking:
Related Tickets: Differential Revisions:

Description

Nathan Howell posts this code:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
-- Uncomment to compile on GHC 7.8
-- {-# LANGUAGE ImpredicativeTypes #-}
 
module Repro where
 
import Control.Monad.Trans.Cont
import Control.Monad.Trans.State.Lazy
 
newtype AnyContT m a = AnyContT { unAnyContT :: forall r . ContT r m a }
 
class MonadAnyCont b m where
  anyContToM :: (forall r . (a -> b r) -> b r) -> m a
 
instance MonadAnyCont b (AnyContT m) where
  anyContToM _ = error "foo"
 
data DecodeState = DecodeState
 
newtype DecodeAST a = DecodeAST { unDecodeAST :: AnyContT (StateT DecodeState IO) a }
  deriving (MonadAnyCont IO)

Compiling on HEAD produces

[1 of 1] Compiling Repro            ( repro.hs, interpreted )
 
repro.hs:24:13:
    Cannot instantiate unification variable ‛b0’
    with a type involving foralls:
      (forall r. (a1 -> IO r) -> IO r) -> DecodeAST a1
      Perhaps you want ImpredicativeTypes
    In the expression:
        GHC.Prim.coerce
          (anyContToM ::
             (forall (r :: *). (a -> IO r) -> IO r)
             -> AnyContT (StateT DecodeState IO) a) ::
          forall (a :: *).
          (forall (r :: *). (a -> IO r) -> IO r) -> DecodeAST a
    In an equation for ‛anyContToM’:
        anyContToM
          = GHC.Prim.coerce
              (anyContToM ::
                 (forall (r :: *). (a -> IO r) -> IO r)
                 -> AnyContT (StateT DecodeState IO) a) ::
              forall (a :: *).
              (forall (r :: *). (a -> IO r) -> IO r) -> DecodeAST a
Failed, modules loaded: none.

Two questions:

  1. Should we require users to specify ImpredicativeTypes here? Or, should the GeneralizedNewtypeDeriving mechanism (which sometimes is impredicative) just assume the extension?
  1. Can we improve the error message?

I'd like to note that the original example really does require impredicativity -- the question is whether and how to bother the user with this technicality.

Small program note: I've done a lot of stuff with GeneralizedNewtypeDeriving lately but am on holiday until Jan. 6, so don't expect responses!

Change History (16)

comment:1 Changed 20 months ago by nomeata

  • Cc mail@… added

comment:2 Changed 19 months ago by simonpj

  • Cc sweirich@… added

We really want explicit type application here (#4466, #5296). The point is that we want to say "instantiate coerce at these particular types", which happen in this case to be polymorphic. (There is a good reason to be suspicious about filling in unification variables with polytypes, but explicit type application would mean that didn't happen.)

Stephanie has a student working on this, I believe.

Simon

comment:3 Changed 19 months ago by goldfire

Yes, absolutely, explicit type application would make all of this much easier. But, I believe we can still fix this bug without it, once we have some design decisions about the questions I posed originally.

As for question 1: I think it's safe to turn on ImpredicativeTypes over the code produced by GND. This would make using GND easier, and I don't want to bother users with this technicality.

As for question 2: In general, I'm a little worried about error messages that mention coerce yet refer to code that patently does not mention coerce. If we can't get rid of the coerce, could we add some extra context describing the use of GND and perhaps suggesting -ddump-deriv?

comment:4 Changed 19 months ago by nomeata

I thought I had got rid of coerce in error messages when doing GND (#8567)... I’ll have to look.

comment:5 Changed 19 months ago by nomeata

It should have been [95ba5d81/ghc]: We check at deriving time that the Coercible instances are solvable, and report an appropriate error message; any time that there is an error message mentioning coercible (or deriv-generated code in general), that is a bug.

So unless turning on ImpredicativeTypes for deriv’ed code solve the problem, we need to check for this already at deriving phase, and report an error. What would that error say?

comment:6 Changed 19 months ago by simonpj

-XImpredicativeTypes it not a very well-defined flag. It might make this program compile, and I think it'd be safe to enable it for GND-produced code. But it has had no love for many years.

Do give it a try; which would make Q2 moot.

Simon

comment:7 Changed 19 months ago by nomeata

Looking into Q1. There is some code temporarily enabling certain extension (EmptyCase, ScopedTypeVariables and KindSignatures) in renameDeriv, but these just affect the renamer; the error message we see occurs later, and I don’t see how we can enable ImpredicativeTypes in a scoped way, i.e. only applying to the code generated by GND.

comment:8 Changed 19 months ago by goldfire

Bah. I was thinking of exactly that code when I suggested enabling ImpredicativeTypes, but I didn't look closely before making the suggestion. I'll see if I can take a look later this week and come up with an implementation plan.

comment:9 Changed 18 months ago by goldfire

I have an implementation plan:

  • Augment InstBindings with a new field ib_extensions, which will be a list of ExtensionFlag.
  • In tcInstanceMethods, apply these flags using setXOptM.
  • In the is_newtype branch of genInst, set ib_extensions to [Opt_ImpredicativeTypes].
  • Elsewhere, set ib_extensions to [].

Seems quite straightforward once I've examined all the plumbing.

Expect a patch in the next few hours.

comment:10 Changed 18 months ago by Richard Eisenberg <eir@…>

In 674c969c240632da70ed2928fa30c20a9a52e5dc/ghc:

Fix #8631.

This patch allows turning on ImpredicativeTypes while type-checking
the code generated by GeneralizedNewtypeDeriving. It does this
by adding a field ib_extensions to InstBindings, informing the
type-checker what extensions should be enabled while type-checking
the instance.

comment:11 Changed 18 months ago by goldfire

  • Status changed from new to merge

Please merge this into 7.8 -- this bug would annoy users if it stays around. Thanks!

comment:12 Changed 18 months ago by carter

I think i was hit by this when I was trying out LLVM-General on 7.8 RC, https://github.com/bscarlet/llvm-general/issues/83#issuecomment-34557918

comment:13 Changed 18 months ago by Richard Eisenberg <eir@…>

In 02c7135dfce049b53bd38aa35c175302652af507/ghc:

Move test case for #8631 to the correct directory.

comment:14 Changed 18 months ago by goldfire

  • Test Case set to deriving/should_compile/T8631

comment:15 Changed 18 months ago by goldfire

  • Milestone set to 7.8.1
  • Version changed from 7.7 to 7.8.1-rc1

Putting this on Austin's radar for 7.8.1.

comment:16 Changed 18 months ago by thoughtpolice

  • Resolution set to fixed
  • Status changed from merge to closed
Note: See TracTickets for help on using tickets.