forall type gives "not polymorphic enough" error incorrectly

[guest]

> type SFST s a b = a -> ST s b
> newtype SF a b = SF { runSF :: forall s. ST s (SFST s a b) }

When making this into an instance of Arrow, compose works beautifully:

> sfCompose :: SF b c -> SF c d -> SF b d
> sfCompose bc cd = SF sf where
>   sf = do
>     runBc <- runSF bc
>     runCd <- runSF cd
>     return $ \b -> runBc b >>= runCd

but pure gives an odd message:

> sfPure :: (b -> c) -> SF b c
> sfPure f = SF sf where
>     sf = return $ \b -> return (f b)

frp_typebug.lhs:20:12:
    Inferred type is less polymorphic than expected
      Quantified type variable `s' is mentioned in the environment:
	sf :: ST s (b -> ST s c) (bound at frp_typebug.lhs:21:5)
    In the first argument of `SF', namely `sf'
    In the expression: SF sf
    In the definition of `sfPure':
	sfPure f = SF sf
		 where
		     sf = return $ (\ b -> return (f b))

This can be worked around using scoped type variables:

> sfPure2 :: (b -> c) -> SF b c
> sfPure2 (f :: b -> c) = SF sf where
>     sf :: forall s. ST s (SFST s b c) 
>        = return $ \b -> return (f b)

but it's ugly.

[guest]

Sorry about the terrible formatting!

[sorear]

Thanks for the report, but I think I can explain this.

Firstly, and quite unrelatedly, you can use triple braces to request monospace, see my edit to the description.

'sf' has no arguments, so the monomorphism restriction applies. The body of 'sf' is assigned a typing derivation of the form:

Monad m1, Monad m2, f :: b -> c |- return $ \b -> return (f b) : m1 (a -> m2 b)

Because 'm1' and 'm2' are constrained by type classes, the monomorphism restriction forces them to be assigned to fully non-polymorphic types; unfortunately this means that it is insufficiently polymorphic for SF.

Possible workarounds include:

{-# LANGUAGE NoMonomorphismRestriction #-}
-- for older GHC, {-# OPTIONS_GHC -fno-monomorphism-restriction #-}

or:

sfPure :: (b -> c) -> SF b c
sfPure f = SF sf where
     returnST :: a -> ST s a
     returnST = return

     sf = returnST $ \b -> returnST (f b)  -- no type classes, no MR

or the aforementioned explicit annotation approach (explicit annotations disable the MR).

Unfortunately, the monomorphism restriction is specified by the Haskell 98 Language Report, so you're more likely to get results from the Haskell-prime committee than you are from specific implementors.

Stefan

[simonpj]

As Stefan says, this is our old friend the Monomorphism Restriction. Look at the defn of sf. Nothing says that it has anything to do with the ST monad, so it's most general type (which GHC infers) is

  sf :: forall m. Monad m => b -> m c

Since that would be a constrained type, the MR kicks in, and it really gets the type

  sf :: b -> m c

Later GHC discovers that m = ST s, but it's too late: sf is in the environment, monomorphic in m, and that means it's insufficiently polymorphic to be an argument to SF.

This doesn't happen in the defn of sfCompose becuase the runSF calls specify that m = ST s, and that's enough to simplify away the Monad constraint, so MR does not kick in, so the defn can be generalised.

This is a nice example of the MR hurting in an unexpected way. I think it'd be good to collect such examples, so I've started a collection on the  main HaskellWiki MR page.

Meanwhile, your best bet is a type signature, only you can do it a bit less clumsily using a forall to bring the type variables into scope

sfPure2 :: forall b c. (b -> c) -> SF b c
sfPure2 f = SF sf where
     sf :: forall s. ST s (SFST s b c)
     sf = return $ \b -> return (f b)

Or you could just inline sf!

Simon

[guest]

Replying to simonpj:

Meanwhile, your best bet is a type signature, only you can do it a bit less clumsily using a forall to bring the type variables into scope

sfPure2 :: forall b c. (b -> c) -> SF b c
sfPure2 f = SF sf where
     sf :: forall s. ST s (SFST s b c)
     sf = return $ \b -> return (f b)

Interesting. Giving "sf" a type signature was my first idea, so I probably subconciously realized it was MR-related, but it didn't work because b & c weren't in scope. Up until now I believed that these two type signatures are equivalent:

sfPure :: (b -> c) -> SF b c
sfPure2 :: forall b c. (b -> c) -> SF b c

Is there a reason why the former doesn't scope in b & c but the latter does? Actually, I think I see why; the forall limits the lexical scope to the internals of the function, whereas without that you can't immediately tell whether b & c are captured from the higher level environment or are "fresh" type variables to be brought into scope.

Thanks!

[sorear]

It's also to break compatibility - supporting scoped type variables is a semantic change, so it has to be introduced with new syntax, in much the same way that int foo(); and int foo(void); are different in C. Hopefully Haskell-prime will remove the need for this crutch.

[simonpj]

http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html#scoped-type-variables explains the way GHC does scoped type variables. The two type sigs you thought are equivalent, aren't equivalent in this design. Yes, that's odd, but I've been though several designs for scoped type variables and this seems the least bad.

Scoped type variables, in some form, are essential else you simply can't write some type signatures, and that's unacceptable. (Esp with higer rank types.)