20e1deb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix irrelevance bug

Need to check if an implicit argument has a placeholder (i.e. is an unbound implicit) before marking it as irrelevant (we were treating all implicits as irrelevant so giving spurious warnings in some cases!)

commit20e1debdbc9c78ec5855262493e0c40fd9464d6d authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 7 Mar 2015, 17:16 (12 years ago) parent4313def

3 files changed+5−3

compare with master

unifiedsplit

libs/prelude/IO.idr+1−1 src/Idris/AbsSyntax.hs+3−1 src/Idris/Elab/Type.hs+1−1

libs/prelude/IO.idr+1−1

@@ -212,7 +212,7 @@ namespace FFI_Export

212212 DThere : DataDefined x xs t -> DataDefined x (y :: xs) t

213213

214214 data FFI_Base : (f : FFI) -> List (Type, ffi_data f) -> Type -> Type where

215− FFI_ExpType : (def : DataDefined t xs n) -> FFI_Base f xs t

215+ FFI_ExpType : {n : ffi_data f} -> (def : DataDefined t xs n) -> FFI_Base f xs t

216216 FFI_Prim : (prim : ffi_types f t) -> FFI_Base f xs t

217217

218218 %used FFI_ExpType n

src/Idris/AbsSyntax.hs+3−1

@@ -1300,8 +1300,10 @@ getUnboundImplicits i t tm = getImps t (collectImps tm)

13001300 getImps (Bind n (Pi _ t _) sc) imps

13011301 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps

13021302 where

1303+ argInfo n (Imp opt _ _ _) Placeholder

1304+ = (True, PImp 0 True opt n Placeholder)

13031305 argInfo n (Imp opt _ _ _) t'

1304− = (True, PImp (getPriority i t') True opt n t')

1306+ = (False, PImp (getPriority i t') True opt n t')

13051307 argInfo n (Exp opt _ _) t'

13061308 = (InaccessibleArg `elem` opt,

13071309 PExp (getPriority i t') opt n t')

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

@@ -90,7 +90,7 @@ buildType info syn fc opts n ty' = do

9090 let (inaccData, impls) = unzip $ getUnboundImplicits i cty ty

9191 let inacc = inaccessibleImps 0 cty inaccData

9292 logLvl 3 $ show n ++ ": inaccessible arguments: " ++ show inacc ++

93− " from " ++ show (cty, ty)

93+ " from " ++ show cty ++ "\n" ++ showTmImpls ty

9494

9595 putIState $ i { idris_implicits = addDef n impls (idris_implicits i) }

9696 logLvl 3 ("Implicit " ++ show n ++ " " ++ show impls)