@@ -661,8 +661,12 @@ elabClass info syn doc fc constraints tn ps ds
661 (filter clause ds)
661 (filter clause ds)
662 let (methods, imethods)
662 let (methods, imethods)
663 = unzip (map (\ ( x,y,z) -> (x, y)) ims)
663 = 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
664 let cty = impbind ps $ conbind constraints
667 let cty = impbind ps $ conbind constraints
668+ $ pibind (map (\ (n, ty) -> (mdec n, ty)) methods)
665− $ pibind methods constraint
669+ constraint
666 let cons = [("", cn, cty, fc)]
670 let cons = [("", cn, cty, fc)]
667 let ddecl = PDatadecl tn tty cons
671 let ddecl = PDatadecl tn tty cons
668 logLvl 5 $ "Class data " ++ showDImp True ddecl
672 logLvl 5 $ "Class data " ++ showDImp True ddecl
@@ -685,6 +689,11 @@ elabClass info syn doc fc constraints tn ps ds
685 nodoc (n, (_, o, t)) = (n, (o, t))
689 nodoc (n, (_, o, t)) = (n, (o, t))
686 pibind [] x = x
690 pibind [] x = x
687 pibind ((n, ty): ns) x = PPi expl n ty (pibind ns x)
691 pibind ((n, ty): ns) x = PPi expl n ty (pibind ns x)
693+ mdec (UN n) = (UN ('!':n))
694+ mdec (NS x n) = NS (mdec x) n
688 impbind [] x = x
697 impbind [] x = x
689 impbind ((n, ty): ns) x = PPi impl n ty (impbind ns x)
698 impbind ((n, ty): ns) x = PPi impl n ty (impbind ns x)
690 conbind (ty : ns) x = PPi constraint (MN 0 "c") ty (conbind ns x)
699 conbind (ty : ns) x = PPi constraint (MN 0 "c") ty (conbind ns x)