git.iko.soy/Idris-dev
on master help sign in
Make sure all patterns are top level

Need to call 'liftPats' then order them so that all implicits appear in the right place - we weren't doing this right at the end of elaboration so some implicits which should have been inferred were not. This fixes some mysterious 'No such variable' errors.

commitc3f827fddd198ac2dff7e666ba24e6062a9ec7d7 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 26 Mar 2015, 21:46 (12 years ago) parentfaa95c0
2 files changed+8−6
compare with master
unifiedsplit
libs/prelude/IO.idr+4−2 src/Idris/ElabTerm.hs+4−4
libs/prelude/IO.idr+4−2
@@ -50,8 +50,10 @@ applyEnv : (env : FEnv ffi xs) ->
5050applyEnv [] f = f
5151applyEnv (x@(_, _) :: xs) f = applyEnv xs (f x)
5252
53−mkForeignPrim : ForeignPrimType xs env t
54−-- compiled as primitive
53+mkForeignPrim : {xs : _} -> {ffi : _} -> {env : FEnv ffi xs} -> {t : Type} ->
54+ ForeignPrimType xs env t
55+-- compiled as primitive. Compiler assumes argument order, so make it
56+-- explicit here.
5557
5658%inline
5759foreign_prim : (f : FFI) ->
src/Idris/ElabTerm.hs+4−4
@@ -119,9 +119,9 @@ build ist info emode opts fn tm
119119 if inf then return ()
120120 else lift (Error e)
121121
122− when tydecl (do update_term orderPats
123− mkPat)
124−-- update_term liftPats)
122+ when tydecl (do mkPat
123+ update_term liftPats
124+ update_term orderPats)
125125 EState is _ impls <- getAux
126126 tt <- get_term
127127 let (tm, ds) = runState (collectDeferred (Just fn) tt) []
@@ -475,7 +475,7 @@ elab ist info emode opts fn tm
475475 _ -> True
476476 -- this is to stop us resolve type classes recursively
477477 -- trace (show (n, guarded)) $
478− if (tcname n && ina) then erun fc $ do patvar n; -- update_term liftPats
478+ if (tcname n && ina) then erun fc $ do patvar n; update_term liftPats
479479 else if (defined && not guarded)
480480 then do apply (Var n) []; solve
481481 else try (do apply (Var n) []; solve)