GitLab

Motivation

It seems to me that MonoLocalBinds is too aggressive in avoiding generalisation. Please observe the example below. In pFG1, pBD is not generalised. The reason is roughly because pBArg does not have a monomorphic type signature, and indeed providing one, as in pFG2, leads to a generalised definition.

But this seems too aggressive to me. In pFG1 the type of pBArg is known and monomorphic. Its type occurs in the type signature of pFG1! Could we generalise pBD in this case?

This is a simplified and anonymised version of real word code. This really does happen. The cause puzzled me and I'm an experienced Haskell user. I feel bad for a less experienced colleague who might try something similar but would receive a type error for code which seems like it really ought to type check.

Proposal

Extend the definition of "closed" to encompass lambda bound variables whose type, from the explicit type signature of the lambda, is known and contains no free type variables.

Notes

This issue was discussed between @tomjaguarpaw1 and @rae on Haskell-Cafe.

I have included pFG3 for information only in case anyone is curious what happens in the polymorphic case. They don't work even with an explicit type signature.

Example

{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- This code came up in the context of writing a parser, but that's
-- not terribly important

import Prelude hiding ((<$>))

data B = B

data D f = GF AP f
         | DF AM f

data AM = AM
data AP = AP

pB :: Parser B
pB = Parser

-- Does not type check
pFG1 :: Parser B -> Parser (D B)
pFG1 pBArg = pBD GF AP <|> pBD DF AM
  where pBD f p = f p <$> pBArg

-- Does type check
pFG2 :: Parser B -> Parser (D B)
pFG2 pBArg = pBD GF AP <|> pBD DF AM
  where pBArg' :: Parser B
        pBArg' = pBArg
        pBD f p = f p <$> pBArg'

-- Does not type check
pFG3 :: forall b. Parser b -> Parser (D b)
pFG3 pBArg = pBD GF AP <|> pBD DF AM
  where pBArg' :: Parser b
        pBArg' = pBArg
        pBD f p = f p <$> pBArg'

-- The specifics of the parser don't matter
data Parser a = Parser

(<|>) :: Parser a -> Parser a -> Parser a
(<|>) _ _ = Parser

(<$>) :: (a -> b) -> Parser a -> Parser b
(<$>) _ _ = Parser