d40cd6f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Check for duplicate names in Can't Convert

Fixes #1804

commitd40cd6f4825f77f0f257abd35709ec23864405d0 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 24 Dec 2014, 21:24 (12 years ago) parent2e6b5e0

5 files changed+31−19

compare with master

unifiedsplit

src/Idris/Core/TT.hs+9−7 src/Idris/Delaborate.hs+19−10 src/Idris/Elab/Clause.hs+1−1 src/Idris/Elab/Utils.hs+1 test/reg054/expected+1−1

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

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

10871087

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

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

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

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

1092− ++ freeNames t

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

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

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

1096−freeNames _ = []

1090+freeNames t = nub $ freeNames' t

1091+ where

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

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

1094+ ++ freeNames' t

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

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

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

1098+ freeNames' _ = []

10971099

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

10991101arity :: TT n -> Int

src/Idris/Delaborate.hs+19−10

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

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

212212 indented (pprintErr' i e) <>

213213 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

215218 text "Can't convert" <>

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

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

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

220+ x)) <$>

218221 text "with" <>

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

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

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

223+ y)) <>

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

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

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

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

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

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

333336

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

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

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

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

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

342341 where

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

344343 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

346350 = do idx <- get

347351 put (idx + 1)

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

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

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

351355

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+

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

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

354363 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

700700 let constv = next_tvar ctxt

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

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

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

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

704704 return ()

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

706706 i <- getIState

src/Idris/Elab/Utils.hs+1

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

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

3131 Error e -> tfail (At fc e)

3232 OK x -> return x

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

3334 addConstraints fc cs

3435 return (tm, ty)

3536

test/reg054/expected+1−1

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

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

66 No explicit types on left hand side: Char

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

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

8+ [94mMaybe[0m a1

99with

1010 [95ma[0m