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

libs/prelude/IO.idr+1−1

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

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

213

214 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

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

217

218 %used FFI_ExpType n

src/Idris/AbsSyntax.hs+3−1

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

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

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

1302 where

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

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

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

1305 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')

1305 argInfo n (Exp opt _ _) t'

1307 argInfo n (Exp opt _ _) t'

1306 = (InaccessibleArg `elem` opt,

1308 = (InaccessibleArg `elem` opt,

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

1309 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

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

91 let inacc = inaccessibleImps 0 cty inaccData

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

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

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

94

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

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