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.

libs/prelude/IO.idr

@@ -50,8 +50,10 @@ applyEnv : (env : FEnv ffi xs) ->
 applyEnv [] f = f
 applyEnv (x@(_, _) :: xs) f = applyEnv xs (f x)
 
-mkForeignPrim : ForeignPrimType xs env t
--- compiled as primitive
+mkForeignPrim : {xs : _} -> {ffi : _} -> {env : FEnv ffi xs} -> {t : Type} ->
+                ForeignPrimType xs env t
+-- compiled as primitive. Compiler assumes argument order, so make it
+-- explicit here.
 
 %inline
 foreign_prim : (f : FFI) -> 

src/Idris/ElabTerm.hs

@@ -119,9 +119,9 @@ build ist info emode opts fn tm
                                      if inf then return ()
                                             else lift (Error e)
 
-         when tydecl (do update_term orderPats
-                         mkPat)
---                          update_term liftPats)
+         when tydecl (do mkPat
+                         update_term liftPats
+                         update_term orderPats)
          EState is _ impls <- getAux
          tt <- get_term
          let (tm, ds) = runState (collectDeferred (Just fn) tt) []
@@ -475,7 +475,7 @@ elab ist info emode opts fn tm
                                _ -> True
            -- this is to stop us resolve type classes recursively
              -- trace (show (n, guarded)) $
-             if (tcname n && ina) then erun fc $ do patvar n; -- update_term liftPats
+             if (tcname n && ina) then erun fc $ do patvar n; update_term liftPats
                else if (defined && not guarded)
                        then do apply (Var n) []; solve
                        else try (do apply (Var n) []; solve)