javac cannot find symbol with forall-types

[mabre]

The following code compiles with frege3.23.888-g4e22ab6 (and ghc with XRankNTypes and small syntax changes), but doesn’t compile with 3.24.61.

module ParsecCompileBug2 where                   

makeTokenParser :: LanguageDef st -> TokenParser st
makeTokenParser languageDef
    = TokenParser{ lexeme = lexeme
                 , whiteSpace = whiteSpace
                 , natural = natural
                 , integer = integer }
    where

    lexeme :: forall a st. CharParser st a -> CharParser st a
    lexeme p = do { x <- p; whiteSpace; return x }

    whiteSpace :: forall st. CharParser st ()
    whiteSpace
        | noLine && noMulti = undefined
        | noLine            = undefined
        where
          noLine   = null []
          noMulti  = null (languageDef.commentStart)

    integer = lexeme int
    natural = lexeme nat
    int = undefined
    nat = undefined

-- Necessary Definitions
data LanguageDef st = LanguageDef { commentStart :: String }                           

data TokenParser st = TokenParser { whiteSpace :: CharParser st ()
                                  , lexeme     :: forall a. CharParser st a -> CharParser st a
                                  , integer    :: CharParser st Integer
                                  , natural    :: CharParser st Integer }

type CharParser st a    = GenParser Char st a
type Parser a           = GenParser Char () a
data GenParser tok st a = Parser (State tok st -> Consumed (Reply tok st a))
data Consumed a     = Consumed a
data State tok st   = State
data Reply tok st a = Ok a (State tok st) String

instance Monad (GenParser tok st) where
  pure x     = undefined
  p >>= f    = undefined

W ParsecCompileBug2.fr:17: guard (noLine) may evaluate to false.
calling: javac -cp /home/mabre/Downloads/frege/frege3.24.61.jar:/tmp/ -d /tmp/ -sourcepath . -encoding UTF-8 /tmp//ParsecCompileBug2.java 
/tmp/ParsecCompileBug2.java:1059: error: incompatible types: TLanguageDef<st#1> cannot be converted to TLanguageDef<st#2>
      if (noLine$7628 && PreludeList.IListView_StringJ.<Character>$null(TLanguageDef.<st>commentStart(arg$1.call()))) {
                                                                                                                ^
  where st#1,st#2 are type-variables:
    st#1 extends Object declared in method <st#1>makeTokenParser(Lazy<TLanguageDef<st#1>>)
    st#2 extends Object declared in method <st#2>whiteSpace$7621()
/tmp/ParsecCompileBug2.java:1093: error: cannot find symbol
                  let$8183.lexeme$7620
                          ^
  symbol:   variable lexeme$7620
  location: variable let$8183 of type Let$8183
Note: Some messages have been simplified; recompile with -Xdiags:verbose to get full output
2 errors
E ParsecCompileBug2.fr:44: java compiler errors are
    most likely caused by erroneous native definitions

When removing the type annotations for lexeme and whiteSpace (which still compiles with ghc and matched the original parsec code), I get type errors instead:

E ParsecCompileBug2.fr:22: type `Integer` is not as
    polymorphic as suggested in the annotation where just
    `a` is announced.
E ParsecCompileBug2.fr:22: type error in expression lexeme undefined
    type is : CharParser t1 a
    expected: CharParser t1 Integer
E ParsecCompileBug2.fr:23: type `Integer` is not as
    polymorphic as suggested in the annotation where just
    `a` is announced.
E ParsecCompileBug2.fr:23: type error in expression lexeme undefined
    type is : CharParser t1 a
    expected: CharParser t1 Integer

When adding type annotations for integer and natural (CharParser st Integer), the errors are these:

E ParsecCompileBug2.fr:23: type `st` is not as polymorphic as
    suggested in the annotation where just `st` is
    announced.
E ParsecCompileBug2.fr:23: type error in expression lexeme int
    type is : CharParser st Integer
    expected: CharParser st Integer
E ParsecCompileBug2.fr:5: type `Integer` is not as
    polymorphic as suggested in the annotation where just
    `a` is announced.
E ParsecCompileBug2.fr:5: type error in expression lexeme
    type is : CharParser st a
    expected: CharParser st Integer
E ParsecCompileBug2.fr:5: type `Integer` is not as
    polymorphic as suggested in the annotation where just
    `a` is announced.
E ParsecCompileBug2.fr:5: type error in expression lexeme
    type is : CharParser st Integer
    expected: CharParser st a
E ParsecCompileBug2.fr:5: type `st` is not as polymorphic as
    suggested in the annotation where just `st` is
    announced.
E ParsecCompileBug2.fr:5: type error in expression TokenParser whiteSpace lexeme integer natural
    type is : TokenParser st
    expected: TokenParser st
E ParsecCompileBug2.fr:5: type `st` is not as polymorphic as
    suggested in the annotation where just `st` is
    announced.
E ParsecCompileBug2.fr:5: type error in expression let integer=lexeme int in ...
    type is : TokenParser st
    expected: TokenParser st
E ParsecCompileBug2.fr:5: type `st` is not as polymorphic as
    suggested in the annotation where just `st` is
    announced.
E ParsecCompileBug2.fr:5: type error in expression let natural=lexeme nat in ...
    type is : TokenParser st
    expected: TokenParser st
E ParsecCompileBug2.fr:5: type `st` is not as polymorphic as
    suggested in the annotation where just `st` is
    announced.
E ParsecCompileBug2.fr:5: type error in expression let lexeme=λp -> >>= p (λx -> >> whiteSpace (return x)) in ...
    type is : TokenParser st
    expected: TokenParser st
E ParsecCompileBug2.fr:5: type `st` is not as polymorphic as
    suggested in the annotation where just `st` is
    announced.
E ParsecCompileBug2.fr:5: type error in expression let whiteSpace=let noLine=null [] in ... in ...
    type is : TokenParser st
    expected: TokenParser st
E ParsecCompileBug2.fr:5: type `st` is not as polymorphic as
    suggested in the annotation where just `st` is
    announced.
E ParsecCompileBug2.fr:5: type error in expression let int=undefined in ...
    type is : TokenParser st
    expected: TokenParser st
E ParsecCompileBug2.fr:5: type `st` is not as polymorphic as
    suggested in the annotation where just `st` is
    announced.
E ParsecCompileBug2.fr:5: type error in expression let nat=undefined in ...
    type is : TokenParser st
    expected: TokenParser st
E ParsecCompileBug2.fr:4: type `st` is not as polymorphic as
    suggested in the annotation where just `st` is
    announced.
E ParsecCompileBug2.fr:4: type error in expression λlanguageDef -> let nat=undefined in ...
    type is : TokenParser st
    expected: TokenParser st

(The messages where type is = expected are not very helpful.)

[Ingo60]

@mabre, congratulations, you're the first one to report such an error for the alpha version.
Thank you for the extensive description.

Let me see what I can do here.

[Ingo60]

Here we go.

First, the workaround: https://github.com/Frege/frege/blob/bounds/tests/comp/Issue270.fr

There are actually 2 errors you have found (see below). The workaround for the first one is to not use type variables in let bound functions that have the same name as the ones used in the enclosing function.
The workaround for the second error is to do an explicit eta expansion. i.e. change

    lexeme = lexeme,

to

   lexeme = \p -> lexeme p,

Here is an explanation:

Problem 1

When the names of type variables of let bound functions is the same
as in the enclosing function, errors may(!) occur. In our case, whiteSpace references
languageDef and while the frege compiler can sort out its type variables quite fine
in type checking, it ruins it in code generation by doing something stupid like:

final<st> ... makeTokenParser(LanguageDef<st> languageDef) {
    class Let {
           final<st> ... whiteSpace(....) { 
                      .... languageDef.<st>commentStart ... 
           }
           ...
     }
     ...
}

and the Java compiler rightfully complains that the outer st and the inner st don't match. In fact, they're supposed to be different types, so in the end what we have here is a simple scoping error.

This can only happen in the rare cases where type annotated let bindings cannot be
lifted to the top level.

Solution: alpha conversion of annotations for let bound functions. (This should also
better the error message problem "type is st, expected st")

Problem 2

For some reason the "lexeme" function is generated as a method, but the code generator thinks under certain circumstances it is just a lambda-expression. It does it right when lexeme is applied, rather than just referenced, though.

This must be
a (hopefully minor) glitch in the let-code generator. Polymorphic functions must always be methods, because intrduction of type variables on merely members is forbidden in Java.

Other remarks

The many type errors you get when you take away the type annotations for whiteSpace or lexeme are justified, since he Frege compiler does not generalize let bindings. However, as it stands, there is no monomorphic type for those functions, and hence there must be annotations.
For more info on this: https://github.com/Frege/frege/wiki/GHC-Language-Options-vs.-Frege#let-generalisation (the Frege compiler behaves like GHC with -XMonoLocalBindings)

I'll try to fix both problems and check back when I have done so. In the meantime you can hopefully live with the workarounds.

[mabre]

Wow, thank you very much for the prompt answer and the thorough description.