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.a...@ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
