Wrong error message when using forall in constraints

changed weight to 5

assigned to @simonpj

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.

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 (closed), #2893 (closed), #2456 (closed). 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.

mentioned in commit 8197fe80

closed

Done, and tests added.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed
Test case	→ typecheck/should_fail/T7019, T7019a

mentioned in issue #9195 (closed)

This compiles using Data.Constraint.Forall for the record:

import Data.Constraint
import Data.Constraint.Forall

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

class    c (Free c a) => C c a
instance c (Free c a) => C c a

instance Applicative (Free c) where
  pure :: a -> Free c a
  pure a = Free ($ a)

  (<*>) :: Free c (a -> b) -> (Free c a -> Free c b)
  Free f <*> Free g = Free (\bfr -> f (\ab -> g (bfr . ab)))

instance Forall (C c) => Monad (Free c) where
  return :: a -> Free c a
  return a = Free ($ a)

  (>>=) :: forall a b. Free c a -> (a -> Free c b) -> Free c b
  Free f >>= g = f g \\
    inst @(C c) @b

joinFree :: forall c a. Forall (C c) => Free c (Free c a) -> Free c a
joinFree (Free f) = f id \\
  inst @(C c) @a

added Pnormal label

Trac field	Value
Version	7.4.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

Wrong error message when using forall in constraints

Child items 0

Activity