@@ -661,8 +661,12 @@ elabClass info syn doc fc constraints tn ps ds
661661 (filter clause ds)
662662 let (methods, imethods)
663663 = unzip (map (\ ( x,y,z) -> (x, y)) ims)
664+ -- build instance constructor type
665+ -- decorate names of functions to ensure they can't be referred
666+ -- to elsewhere in the class declaration
664667 let cty = impbind ps $ conbind constraints
665− $ pibind methods constraint
668+ $ pibind (map (\ (n, ty) -> (mdec n, ty)) methods)
669+ constraint
666670 let cons = [("", cn, cty, fc)]
667671 let ddecl = PDatadecl tn tty cons
668672 logLvl 5 $ "Class data " ++ showDImp True ddecl
@@ -685,6 +689,11 @@ elabClass info syn doc fc constraints tn ps ds
685689 nodoc (n, (_, o, t)) = (n, (o, t))
686690 pibind [] x = x
687691 pibind ((n, ty): ns) x = PPi expl n ty (pibind ns x)
692+
693+ mdec (UN n) = (UN ('!':n))
694+ mdec (NS x n) = NS (mdec x) n
695+ mdec x = x
696+
688697 impbind [] x = x
689698 impbind ((n, ty): ns) x = PPi impl n ty (impbind ns x)
690699 conbind (ty : ns) x = PPi constraint (MN 0 "c") ty (conbind ns x)