be57f4a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix unbound implicit rules

We were automatically binding names in function position, which is not what the tutorial says and not what I intended... this can lead to strange error reports. Fixes #913

commitbe57f4a2652c5639ddb44264bea1d7f0df4c5306 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 6 Mar 2014, 15:49 (13 years ago) parenta7217f1

2 files changed+11−5

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+10−4 src/Idris/Delaborate.hs+1−1

src/Idris/AbsSyntax.hs+10−4

@@ -1250,18 +1250,24 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

12501250 | otherwise = x : dropAll xs ys

12511251 dropAll [] ys = []

12521252

1253+ -- Find names in argument position in a type, suitable for implicit

1254+ -- binding

1255+ -- Not the function position, but do everything else...

1256+ implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv) (map getTm args)

1257+ implNamesIn uv t = namesIn uv ist t

1258+

12531259 imps top env (PApp _ f as)

12541260 = do (decls, ns) <- get

12551261 let isn = concatMap (namesIn uvars ist) (map getTm as)

12561262 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

12571263 imps top env (PPi (Imp l _ _) n ty sc)

1258− = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]

1264+ = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]

12591265 (decls , ns) <- get

12601266 put (PImp (getPriority ist ty) True l n Placeholder : decls,

12611267 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

12621268 imps True (n:env) sc

12631269 imps top env (PPi (Exp l _ _) n ty sc)

1264− = do let isn = nub (namesIn uvars ist ty ++ case sc of

1270+ = do let isn = nub (implNamesIn uvars ty ++ case sc of

12651271 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

12661272 _ -> [])

12671273 (decls, ns) <- get -- ignore decls in HO types

@@ -1269,7 +1275,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

12691275 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

12701276 imps True (n:env) sc

12711277 imps top env (PPi (Constraint l _) n ty sc)

1272− = do let isn = nub (namesIn uvars ist ty ++ case sc of

1278+ = do let isn = nub (implNamesIn uvars ty ++ case sc of

12731279 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

12741280 _ -> [])

12751281 (decls, ns) <- get -- ignore decls in HO types

@@ -1277,7 +1283,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

12771283 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

12781284 imps True (n:env) sc

12791285 imps top env (PPi (TacImp l _ scr) n ty sc)

1280− = do let isn = nub (namesIn uvars ist ty ++ case sc of

1286+ = do let isn = nub (implNamesIn uvars ty ++ case sc of

12811287 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

12821288 _ -> [])

12831289 (decls, ns) <- get -- ignore decls in HO types

src/Idris/Delaborate.hs+1−1

@@ -233,7 +233,7 @@ pprintErr' i (ReflectionFailed msg err) =

233233 text ("This is probably a bug. Please consider reporting it at " ++ bugaddr)

234234

235235annName :: Name -> Doc OutputAnnotation

236−annName n = annName' n (show n)

236+annName n = annName' n (showbasic n)

237237

238238annName' :: Name -> String -> Doc OutputAnnotation

239239annName' n str = annotate (AnnName n Nothing Nothing) (text str)