@@ -1130,19 +1130,22 @@ aiFn :: Bool -> Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
1130aiFn inpat True ist fc f []
1130aiFn inpat True ist fc f []
1131 = case lookupDef f (tt_ctxt ist) of
1131 = case lookupDef f (tt_ctxt ist) of
1132 [] -> Right $ PPatvar fc f
1132 [] -> Right $ PPatvar fc f
1133− alts -> let ialts = lookupCtxt f (idris_implicits ist) in
1133+ alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1134 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1134 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1135 if (not (vname f) || tcname f
1135 if (not (vname f) || tcname f
1136+ || any (conCaf (tt_ctxt ist)) ialts)
1136− || any constructor alts || any allImp ialts)
1137+-- any constructor alts || any allImp ialts))
1137 then aiFn inpat False ist fc f [] -- use it as a constructor
1138 then aiFn inpat False ist fc f [] -- use it as a constructor
1138 else Right $ PPatvar fc f
1139 else Right $ PPatvar fc f
1139 where imp (PExp _ _ _ _) = False
1140 where imp (PExp _ _ _ _) = False
1140 imp _ = True
1141 imp _ = True
1141− allImp [] = False
1142+-- allImp [] = False
1142 allImp xs = all imp xs
1143 allImp xs = all imp xs
1143 constructor (TyDecl (DCon _ _) _) = True
1144 constructor (TyDecl (DCon _ _) _) = True
1144 constructor _ = False
1145 constructor _ = False
1147+ conCaf ctxt (n, cia) = isDConName n ctxt && allImp cia
1146 vname (UN n) = True -- non qualified
1149 vname (UN n) = True -- non qualified
1147 vname _ = False
1150 vname _ = False