Surprising lack of generalisation using MonoLocalBinds
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