To your amusement, I found the following in the Agda source: abstractToConcreteCtx :: ToConcrete a c => Precedence -> a -> TCM c abstractToConcreteCtx ctx x = do scope <- getScope let scope' = scope { scopePrecedence = ctx } return $ abstractToConcrete (makeEnv scope') x where scope = (currentScope defaultEnv) { scopePrecedence = ctx } I am surprised this is a legal form of shadowing. To understand which definition of 'scope' shadows the other, I have to consult the formal definition of Haskell. But I studied computer science to *not* become a lawyer!! -- Andreas Abel <>< Du bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.abel@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/