Two functions compile with type annotations. Remove one annotation - doesn't compile. Remove two - compiles again. Why?

Question

Mind this Reflex program:

{-# LANGUAGE ScopedTypeVariables, RecursiveDo #-}

import Control.Applicative
import Control.Monad
import Control.Monad.IO.Class
import Prelude hiding (div)
import Reflex.Dom
import qualified Data.Map as M

clickMe :: MonadWidget t m => m (Event t ())
clickMe = do
    rec (e,_) <- elAttr' "button" M.empty (display c)
        c :: Dynamic t Int <- count (domEvent Click e)
    return $ domEvent Click e

div :: forall t m a . MonadWidget t m => m a -> m a
div = elAttr "div" ("style" =: "border : 1px solid black")

app :: forall t m . MonadWidget t m => m ()
app = div $ do
    aClicks <- clickMe
    bClicks <- clickMe
    a <- count aClicks
    b <- count bClicks
    l <- combineDyn (\a b -> replicate (a-b) ()) a b
    simpleList l (const clickMe)
    return ()

main = mainWidget app

If you remove the type annotation from either div or app, the program won't compile with a huge, scary type error. If you remove both, it will compile again. From a programmer's perspective, this gives a terrible user experience when someone is trying to incrementally annotate an unannotated program. It makes no sense that adding a correct type annotation to an unannotated term causes a compiler error, and it leads the programmer to think he got the type wrong.

This is the error you get by removing div's annotation.

Those are the inferred types.

Why this happens?

Answer 1

This is due to to the monomorphism restriction. When the compiler is typechecking a top-level binding without a type annotation, it will not assign a polymorphic type if that type has a constraint and the function has no syntactic argument, which is the case for both of your functions.

However, if you include neither type signature, it still doesn't compile. In your case, you gave it some extra information (the foo = [app, _] part) and for some reason it chose to pick a monomorphic type - I don't know what changed about your environment but that isn't standard behaviour.

Here is a simple file distilling the issue you are having:

{-# LANGUAGE RankNTypes, KindSignatures, MultiParamTypeClasses, FunctionalDependencies #-}

module Test where 

import Prelude hiding (div)

class MonadWidget t (m :: * -> *) | m -> t 

div :: forall t m a . MonadWidget t m => m a -> m a
div = (undefined :: forall t m a . MonadWidget t m => m a -> m a)

app :: forall t m . MonadWidget t m => m ()
app = (div (undefined :: forall t m . MonadWidget t m => m ())
        :: forall t m . MonadWidget t m => m () )

If you comment out either type signature, or both, you will be met with an error. However, comment out any top-level type signature, but run this with ghc -XNoMonomorphismRestriction Test.hs and it will compile successfully in every configuration. Here are a few tests.

Answer 2

As Reid Barton noted in comments, this is due to The Dreaded Monomorphism Restriction.

Here is simplified example:

foo :: Monad m => m a -> m a
foo = (>>= return)

bar :: Monad m => m ()
bar = foo (return ())

When monomorphism restriction enabled and foo's type signature commented:

• GHC tries to assign monomorphic type to to foo and fails because there is no default Monad instance:

No instance for (Monad m0) arising from a use of ‘>>=’
The type variable ‘m0’ is ambiguous

• using foo at bar leads to another error which I cannot explain

Couldn't match type ‘m0’ with ‘m’
because type variable ‘m’ would escape its scope

Adding {-# LANGUAGE NoMonomorphismRestriction #-} pragma fixes this and allows to add type signatures incrementally.