Wrong error message when using forall in constraints

[sjoerd_visscher]

I tried this in GHC 7.4.1:

{-# LANGUAGE ConstraintKinds, RankNTypes, UndecidableInstances #-}

newtype Free c a = Free { runFree :: forall r. c r => (a -> r) -> r }

type C c = forall a. c (Free c a)
instance C c => Monad (Free c) where
  return a = Free ($ a)
  Free f >>= g = f g

Which gives this error:

    Could not deduce (c (Free c b)) arising from a use of `f'
    from the context (C c)

So apparently the forall is silently dropped.

Without UndecidableInstances? the error is:

    Illegal irreducible constraint forall a. c (Free c a)
    in superclass/instance head context (Use -XUndecidableInstances to permit this)

giving the impression that it is allowed.

[sjoerd_visscher]

Apparently it is allowed to use forall in constraints (I just saw that  here). I used the type synonym as a workaround, but that's not needed, so here's a simplified case:

{-# LANGUAGE ConstraintKinds, RankNTypes, UndecidableInstances #-}

import Data.Monoid

newtype Free a = Free { runFree :: forall r. Monoid r => (a -> r) -> r }

instance (forall a. Monoid (Free a)) => Monad (Free) where
  return a = Free ($ a)
  (>>=) = runFree

gives the error

    Could not deduce (Monoid (Free b)) arising from a use of `runFree'
    from the context (forall a. Monoid (Free a))

I replaced the constaint variable with Monoid, to check that that's not the problem. So this new version of course has a simple workaround, but that workaround is not available in the constraint variable version.

[simonpj]

GHC does not support polymorphic constraints to the left of an arrow. The StackOverflow thread you point to contains this program:

{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE Rank2Types           #-}
{-# LANGUAGE ConstraintKinds      #-}
{-# LANGUAGE UndecidableInstances #-}

module T7019a where

class Context c where
  func1 :: c -> String

class (forall b. Context (Associated a b))   -- URK!
   => Class a where
  data Associated a :: * -> *

newtype ClassTest = ClassTest { runClassTest :: String }

instance (forall b. Context (Associated ClassTest b))  -- URK!
      => Class ClassTest where
  data Associated ClassTest b = ClassTestAssoc b (b -> ClassTest)

instance Context (Associated ClassTest b) where
  func1 (ClassTestAssoc b strFunc) = runClassTest $ strFunc b

main = putStr . func1 $ ClassTestAssoc 37 (ClassTest . show)

I'm astonished that this program typechecks. It certainly shouldn't. We have not begun to think about constraints like (forall b. (Associated ClassTest b)) I'm afraid.

Actually, your Monoid example makes a lot more sense, but can't you just have a top-level instance

instance Monoid (Free a) where ...(not sure)....

in which case you are fine.

Wanting foralls on the left of an arrow is not stupid. See #5927, #2893, #2456. But it's not going to happen soon, because I don't know how to specify or implement it. (Which is not to say that someone else may not be able to crack it.)

Meanwhile, these programs should be rejected, and I'll add the tests so that they are.

[simonpj]

Done, and tests added.