ongoing: preparations to fix 270

frege/compiler/common/Types.fr

@@ -9,7 +9,7 @@ import  frege.compiler.types.Types as T
 import  Compiler.types.Global as G
 import  Compiler.types.QNames (QName)
 import  Compiler.types.Positions (Position, getpos)
--- import  Compiler.types.Packs(pPreludeBase)
+import  Compiler.common.Binders
 import  frege.compiler.classes.Nice(Nice)
 
 --- tell if the 'SigmaT' represents a function type. 
@@ -219,6 +219,61 @@ sigmaKind (ForAll _ rho) = rhoKind rho
 rhoKind RhoFun{} = KType
 rhoKind RhoTau{tau} = tauKind tau
 
+{--
+    Alpha conversion of a sigma.
+    
+    We don't want inner *forall*s and sigmas for fields and let bound functions
+    have type variable names that are already used further outwards. The reason is that while
+    the Frege compiler never confuses different type variables just because they
+    have the same name, this is not so in Java code. Here, we don't have any means to
+    distinguish type variables *except* by name. And when we use that name, it will always 
+    refer to the innermost introduction of that type variable.
+    
+    See also 'https://github.com/Frege/frege/issues/270 Issue #270'
+    
+    We change variable names by drawing a unique name from 
+    the latin letter supply and appending a number.
+    This way, no type variable name created during generalization will ever conflict
+    with a renamed one. 
+
+    This can still lead to errors when the outer function is not annotated, and the inner one
+    uses type variables from the same character set that will be used in quantification. Such
+    variables are potential duplicates and must be replaced precautionally.
+
+    Therefore, we need the following parameters:
+    
+    1) the names to avoid (from outer sigmas).
+    2) a 'Regex' that describes potential duplicates. If the outer 'Sigma' is indeed
+    annotated, this can be a 'Regex' that would never match any type variable name. Otherwise,
+    it should match every element of the supply that is currently in use.
+    
+    Of course, we simply encode this with a property function that tells us whether a certain
+    variable must be avoided and needs replacement. 
+    
+    Because the renamings of user supplied 'Sigma's can lead to hard to understand error
+    messages, there should be a warning when the 'Sigma' was actually alpha-converted. 
+-}
+
+avoidSigma avoid (ForAll tvs rho) = ForAll ntvs (avoidRho (\c -> avoid c ||  c `elem` new) rho')
+    where
+        old = map _.var tvs                     -- old variables
+        binders = [ bn |    b ← Binders.allAsciiBinders, 
+                            n ← [1..9],
+                            let {bn = b ++ show n},
+                            not (avoid bn),
+                            bn `notElem` old    -- safe new variable names
+                  ]                           
+        bads = filter avoid old                 -- the variables that need replacement
+        reps = Map.fromList (zip bads binders)  -- a substitution for variable names
+        rnvar v tv = tv.{var=v,                 -- rename a variable 
+                         kind ← substKind (Map.singleton tv.var tv')}
+            where tv' = tv.{var=v, kind=KType}      
+        new = undefined
+        avoidRho = undefined
+        rho' = rho
+        ntvs = tvs
+--        rho' = substRho rep rho
+--        rep  = fromList [ (tv.var, rename outer tv) | tv ← tvs, tv.var `elem` outer, 
 
 {--
     > sigInst subst sigma

tests/comp/Issue270.fr

@@ -29,12 +29,12 @@ module tests.comp.Issue270 where
 
 makeTokenParser :: LanguageDef st -> TokenParser st
 makeTokenParser languageDef
-    = TokenParser{ lexeme = \p → lexeme p, 
+    = TokenParser{ lexeme = lexeme, 
                    whiteSpace = whiteSpace, 
                    natural = natural,
                    integer = integer, }
     where
-    whiteSpace :: forall st'. CharParser st' ()
+    whiteSpace :: forall st. CharParser st ()
     whiteSpace
         | noLine && noMulti = undefined
         | noLine            = undefined
@@ -47,7 +47,7 @@ makeTokenParser languageDef
     int = undefined
     nat = undefined
 
-    lexeme :: forall a st'. CharParser st' a -> CharParser st' a
+    lexeme :: forall a st. CharParser st a -> CharParser st a
     lexeme  p = do { x <- p; whiteSpace; return x }