solved problem1 of #270

frege/compiler/Typecheck.fr

@@ -99,6 +99,7 @@ import  Compiler.common.Errors as E()
 import  Compiler.common.Types  as TH
 import  Compiler.common.Resolve as R(weUse)
 import  Compiler.common.SymbolTable
+import  Compiler.common.Binders(avoidBinders)
 
 import  Compiler.classes.Nice
 
@@ -266,7 +267,8 @@ checkgroup  nms = do
 checkgroup7 nms = do
     g <- getST
     E.logmsg TRACEZ Position.null (text ("typechecking group: " ++ joined " " (map (flip QName.nice g) nms)))
-    syms <- mapSt findV nms
+    unless (null g.typEnv) do
+        mapSt findV nms >>= mapM_ renameSigma
     -- we set up typEnv with the names of the group members so that 'envTvs' will find them
     changeST Global.{typEnv <- (nms ++)}
 
@@ -510,10 +512,27 @@ substInst (lit@Lit{pos, kind, value, typ=Just (ForAll [] rho)})
       not (null rho.context) = pure (Right lit.{typ=Just (ForAll [] rho.{context=[]})})
 substInst x = stio (Left x)
 
+renameSigma ∷ Symbol -> StG ()
+renameSigma sym | sym.name.isLocal && sym.anno = do
+    g   ← getST
+    outer ← mapSt findV g.typEnv
+    let avoid  = \c → c `elem` concatMap (Sigma.vars . Symbol.typ) outer 
+                    || (any (null . Sigma.vars . Symbol.typ) outer && avoidBinders g c)
+        newsym = sym.{typ ← avoidSigma avoid }
+    when (sym.typ.vars != newsym.typ.vars) do
+        E.warn sym.pos (text "Renamed annotation " 
+                            <+> text (sym.typ.nicer g)
+                            </> text "to " <+> text (newsym.typ.nicer g)
+                            </> text "because of (potential) type variable name conflict")
+        changeSym newsym
+    pure ()
+renameSigma other = pure ()
+
 
 checkName nm = do
     g       <- getST
     sym     <- findV nm
+    -- sym     <- if nm.isLocal && sym.anno then renameSigma sym else pure sym
     E.logmsg TRACEZ sym.pos (text ("checkName:  " ++ sym.name.nice g ++ " :: " ++ sym.typ.nice g))
     -- E.logmsg TRACET sym.pos (text ("checkName:  " ++ sym.name.nice g ++ " :: " ++ sym.typ.nice g))
     sigma   <- checkSym sym

frege/compiler/common/Binders.fr

@@ -46,4 +46,9 @@ allBinders g
     | otherwise = allAsciiBinders
     where flags = (Global.options g).flags
 
-
+--- a function that tells if a 'String' is member of the current binders
+avoidBinders g 
+    | isOn flags USEFRAKTUR = ( ~ '^[𝖆𝖇𝖈𝖉𝖊𝖋𝖌𝖍𝖎𝖏𝖐𝖑𝖒𝖓𝖔𝖕𝖖𝖗𝖘𝖙𝖚𝖛𝖜𝖝𝖞𝖟]+$')
+    | isOn flags USEGREEK   = ( ~ '^[αβγδεζηθικλμνξοπρςστυφχψω]$')
+    | otherwise             = ( ~ '^[a-z]$')
+    where flags = (Global.options g).flags

frege/compiler/common/Types.fr

@@ -3,7 +3,7 @@ module frege.compiler.common.Types
         inline (isFun)
     where 
 
-import  Data.TreeMap as Map(member, keys, insert, TreeSet, TreeMap)
+import  Data.TreeMap as Map(member, keys, insert, lookup, TreeSet, TreeMap)
 
 import  frege.compiler.types.Types as T
 import  Compiler.types.Global as G
@@ -246,34 +246,49 @@ rhoKind RhoTau{tau} = tauKind tau
     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],
+        binders = [ bn |    n ← [1..3], 
+                            b ← Binders.allAsciiBinders, 
                             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, 
+        mapped = Map.values reps                -- names of renamed variables
+        ntvs = map (rnTVar reps) tvs            -- rename affected type variables
+        new = map _.var ntvs                    -- the variable names of the new Sigma
+        subst = Map.fromList (zip bads [ tv | tv ← ntvs, tv.var `elem` mapped ]) 
+        rho' = substRho subst rho
+
+avoidRho :: (String → Bool) -> Rho -> Rho
+avoidRho avoid (rhofun@RhoFun{})  = rhofun.{sigma ← avoidSigma avoid, rho ← avoidRho avoid}
+avoidRho avoid (rhotau@RhoTau{})  = rhotau
+
+rnTVar :: TreeMap String String → Tau → Tau
+rnTVar tree (TApp a b)  = TApp (rnTVar tree a) (rnTVar tree b)
+rnTVar tree (t@TCon{})  = t
+rnTVar tree (t@TVar{})  = case lookup t.var tree of
+    Just v  →   t.{kind ← rnKind tree, var=v}
+    Nothing →   t
+rnTVar tree (t@TSig _)  = t
+rnTVar tree (t@Meta _)  = t
+
+rnKind :: TreeMap String String → Kind → Kind
+rnKind tree (KGen t)  = KGen (rnTVar tree t)
+rnKind tree (KApp k1 k2)  = KApp (rnKind tree k1) (rnKind tree k2)
+rnKind tree k  = k
+
 
 {--
     > sigInst subst sigma