d40cd6f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Check for duplicate names in Can't Convert

d40cd6fEdwin Brady12 years ago

src/Idris/Core/TT.hs+9−7

compare with master

unifiedsplit

@@ -1087,13 +1087,15 @@ noOccurrence n t = no' 0 t

1087

1088-- | Returns all names used free in the term

1089freeNames :: Eq n => TT n -> [n]

1090−freeNames (P _ n _) = [n]

1090+freeNames t = nub $ freeNames' t

1091+ where

1092+ freeNames' (P _ n _) = [n]

1091−freeNames (Bind n (Let t v) sc) = nub $ freeNames v ++ (freeNames sc \\ [n])

1093+ freeNames' (Bind n (Let t v) sc) = freeNames' v ++ (freeNames' sc \\ [n])

1092− ++ freeNames t

1094+ ++ freeNames' t

1093−freeNames (Bind n b sc) = nub $ freeNames (binderTy b) ++ (freeNames sc \\ [n])

1095+ freeNames' (Bind n b sc) = freeNames' (binderTy b) ++ (freeNames' sc \\ [n])

1094−freeNames (App f a) = nub $ freeNames f ++ freeNames a

1096+ freeNames' (App f a) = freeNames' f ++ freeNames' a

1095−freeNames (Proj x i) = nub $ freeNames x

1097+ freeNames' (Proj x i) = freeNames' x

1096−freeNames _ = []

1098+ freeNames' _ = []

1097

1099

1098-- | Return the arity of a (normalised) type

1100-- | Return the arity of a (normalised) type

1099arity :: TT n -> Int

1101arity :: TT n -> Int

src/Idris/Delaborate.hs+19−10

@@ -211,13 +211,16 @@ pprintErr' i (CantUnify _ x_in y_in e sc s) =

211 _ -> line <> line <> text "Specifically:" <>

212 indented (pprintErr' i e) <>

213 if (opt_errContext (idris_options i)) then showSc i sc else empty

214−pprintErr' i (CantConvert x y env) =

214+pprintErr' i (CantConvert x_in y_in env) =

215+ let (x_ns, y_ns, nms) = renameMNs x_in y_in

216+ (x, y) = addImplicitDiffs (delab i (flagUnique x_ns))

217+ (delab i (flagUnique y_ns)) in

215 text "Can't convert" <>

218 text "Can't convert" <>

216− indented (annTm x (pprintTerm' i (map (\ (n, b) -> (n, False)) env)

219+ indented (annTm x_ns (pprintTerm' i (map (\ (n, b) -> (n, False)) env)

217− (delab i (flagUnique x)))) <$>

220+ x)) <$>

218 text "with" <>

221 text "with" <>

219− indented (annTm y (pprintTerm' i (map (\ (n, b) -> (n, False)) env)

222+ indented (annTm y_ns (pprintTerm' i (map (\ (n, b) -> (n, False)) env)

220− (delab i (flagUnique y)))) <>

223+ y)) <>

221 if (opt_errContext (idris_options i)) then line <> showSc i env else empty

224 if (opt_errContext (idris_options i)) then line <> showSc i env else empty

222 where flagUnique (Bind n (Pi t k@(UType u)) sc)

225 where flagUnique (Bind n (Pi t k@(UType u)) sc)

223 = App (P Ref (sUN (show u)) Erased)

226 = App (P Ref (sUN (show u)) Erased)

@@ -331,10 +334,6 @@ pprintErr' i (ReflectionFailed msg err) =

331-- Make sure the machine invented names are shown helpfully to the user, so

334-- Make sure the machine invented names are shown helpfully to the user, so

332-- that any names which differ internally also differ visibly

335-- that any names which differ internally also differ visibly

333

336

334−-- FIXME: I can't actually contrive an error to test this! Will revisit later...

335−--

336−-- Issue #1590 in the Issue tracker.

337−-- https://github.com/idris-lang/Idris-dev/issues/1590

338renameMNs :: Term -> Term -> (Term, Term, [Name])

337renameMNs :: Term -> Term -> (Term, Term, [Name])

339renameMNs x y = let ns = nub $ allTTNames x ++ allTTNames y

338renameMNs x y = let ns = nub $ allTTNames x ++ allTTNames y

340 newnames = evalState (getRenames [] ns) 1 in

339 newnames = evalState (getRenames [] ns) 1 in

@@ -342,13 +341,23 @@ renameMNs x y = let ns = nub $ allTTNames x ++ allTTNames y

342 where

341 where

343 getRenames :: [(Name, Name)] -> [Name] -> State Int [(Name, Name)]

342 getRenames :: [(Name, Name)] -> [Name] -> State Int [(Name, Name)]

344 getRenames acc [] = return acc

343 getRenames acc [] = return acc

345− getRenames acc (n@(MN i x) : xs) | UN x `elem` xs

344+ getRenames acc (n@(MN i x) : xs) | rpt x xs

345+ = do idx <- get

346+ put (idx + 1)

347+ let x' = sUN (str x ++ show idx)

348+ getRenames ((n, x') : acc) xs

349+ getRenames acc (n@(UN x) : xs) | rpt x xs

346 = do idx <- get

350 = do idx <- get

347 put (idx + 1)

351 put (idx + 1)

348 let x' = sUN (str x ++ show idx)

352 let x' = sUN (str x ++ show idx)

349 getRenames ((n, x') : acc) xs

353 getRenames ((n, x') : acc) xs

350 getRenames acc (x : xs) = getRenames acc xs

354 getRenames acc (x : xs) = getRenames acc xs

351

355

356+ rpt x [] = False

357+ rpt x (UN y : xs) | x == y = True

358+ rpt x (MN i y : xs) | x == y = True

359+ rpt x (_ : xs) = rpt x xs

360+

352 rename :: [(Name, Name)] -> Term -> Term

361 rename :: [(Name, Name)] -> Term -> Term

353 rename ns (P nt x t) | Just x' <- lookup x ns = P nt x' t

362 rename ns (P nt x t) | Just x' <- lookup x ns = P nt x' t

354 rename ns (App f a) = App (rename ns f) (rename ns a)

363 rename ns (App f a) = App (rename ns f) (rename ns a)

src/Idris/Elab/Clause.hs+1−1

@@ -700,7 +700,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

700 let constv = next_tvar ctxt

701 case LState.runStateT (convertsC ctxt [] crhsty clhsty) (constv, []) of

702 OK (_, cs) -> do addConstraints fc cs

703− logLvl 6 $ "CONSTRAINTS ADDED: " ++ show (constv,cs)

703+ logLvl 6 $ "CONSTRAINTS ADDED: " ++ show cs

704 return ()

705 Error e -> ierror (At fc (CantUnify False clhsty crhsty e [] 0))

706 i <- getIState

src/Idris/Elab/Utils.hs+1

@@ -30,6 +30,7 @@ recheckC_borrowing uniq_check bs fc env t

30 (tm, ty, cs) <- tclift $ case recheck_borrowing uniq_check bs ctxt env (forget t) t of

31 Error e -> tfail (At fc e)

32 OK x -> return x

33+ logLvl 6 $ "CONSTRAINTS ADDED: " ++ show cs

33 addConstraints fc cs

34 addConstraints fc cs

34 return (tm, ty)

35 return (tm, ty)

test/reg054/expected+1−1

@@ -5,6 +5,6 @@ reg054.idr:34:7:When elaborating left hand side of weird:

5When elaborating argument [95mx[0m to Main.weird:

6 No explicit types on left hand side: Char

7reg054.idr:37:9:Can't convert

8− [94mMaybe[0m [95ma[0m

8+ [94mMaybe[0m a1

9with

10 [95ma[0m