@@ -365,12 +365,13 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
365365
366366type EliminatorState = StateT (Map.Map String Int) Idris
367367
368−-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite
368+-- TODO: Rewrite everything to use idris_implicits instead of manual splitting (or in TT)
369369elabEliminator :: [Int] -> Name -> PTerm ->
370370 [(Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name])] ->
371371 ElabInfo -> EliminatorState ()
372372elabEliminator paramPos n ty cons info = do
373373 elimLog $ "Elaborating eliminator"
374+ put (Map.fromList $ zip (concatMap (\(_, p, _, ty, _, _) -> (map show $ boundNamesIn ty) ++ map (show . fst) p) cons ++ (map show $ boundNamesIn ty)) (repeat 0))
374375 let (cnstrs, _) = splitPi ty
375376 let (splittedTy@(pms, idxs)) = splitPms cnstrs
376377 generalParams <- namePis False pms
@@ -389,13 +390,14 @@ elabEliminator paramPos n ty cons info = do
389390 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs
390391 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'
391392 let elimSig = "-- eliminator signature: " ++ showTmImpls eliminatorTy
393+ elimLog elimSig
392394 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)
393395 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses
394396 elimLog $ "-- eliminator definition: " ++ (show . showDeclImp True) eliminatorDef
395397 State.lift $ idrisCatch (elabDecl EAll info eliminatorTyDecl) (\err -> return ())
396398 -- Do not elaborate clauses if there aren't any
397399 case eliminatorClauses of
398− [] -> return ()
400+ [] -> State.lift $ solveDeferred elimDeclName -- Remove meta-variable for type
399401 _ -> State.lift $ idrisCatch (elabDecl EAll info eliminatorDef) (\err -> return ())
400402 where elimLog :: String -> EliminatorState ()
401403 elimLog s = State.lift (logLvl 2 s)
@@ -458,9 +460,9 @@ elabEliminator paramPos n ty cons info = do
458460 freshName key = do
459461 nameMap <- get
460462 let i = fromMaybe 0 (Map.lookup key nameMap)
461− let name = key ++ show i
463+ let name = uniqueName (sUN (key ++ show i)) (map (\(nm, nb) -> sUN (nm ++ show nb)) $ Map.toList nameMap)
462464 put $ Map.insert key (i+1) nameMap
463− return (sUN name)
465+ return name
464466
465467 scrutineeName :: Name
466468 scrutineeName = sUN "scrutinee"
@@ -553,7 +555,7 @@ elabEliminator paramPos n ty cons info = do
553555 let cons' = replaceParams paramPos generalParameters ty
554556 let (args, resTy) = splitPi cons'
555557 implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)
556− consArgs <- namePis True args
558+ consArgs <- namePis False args
557559 let recArgs = findRecArgs consArgs
558560 let recMotives = map applyRecMotive recArgs
559561 let (_, consIdxs) = splitArgPms resTy
@@ -592,7 +594,7 @@ elabEliminator paramPos n ty cons info = do
592594 implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)
593595 let (_, generalIdxs') = splitArgPms resTy
594596 let generalIdxs = map pexp generalIdxs'
595− consArgs <- namePis True args
597+ consArgs <- namePis False args
596598 let lhsPattern = PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ generalIdxs ++ [pexp $ applyCons cnm consArgs])
597599 let recArgs = findRecArgs consArgs
598600 let recElims = map applyRecElim recArgs