Merge pull request #190 from edwinb/various-fixes

Various fixes

src/Core/Binary.idr

@@ -30,7 +30,7 @@ import Data.Buffer
 -- TTC files can only be compatible if the version number is the same
 export
 ttcVersion : Int
-ttcVersion = 29
+ttcVersion = 30
 
 export
 checkTTCVersion : String -> Int -> Int -> Core ()

src/Core/LinearCheck.idr

@@ -215,7 +215,9 @@ mutual
            Just gdef <- lookupCtxtExact (Resolved idx) (gamma defs)
                 | _ => throw (UndefinedName fc n)
            let expand = branchZero
-                          False
+                          (case type gdef of
+                                Erased _ _ => True -- defined elsewhere, need to expand
+                                _ => False)
                           (case definition gdef of
                                 (PMDef _ _ _ _ _) => True
                                 _ => False)

src/Core/TTC.idr

@@ -944,7 +944,8 @@ TTC GlobalDef where
            let refs = map fromList refsList
            def <- fromBuf b
            if isUserName name
-              then do ty <- fromBuf b; eargs <- fromBuf b;
+              then do ty <- fromBuf b
+                      eargs <- fromBuf b;
                       seargs <- fromBuf b; specargs <- fromBuf b
                       iargs <- fromBuf b;
                       vars <- fromBuf b

src/Idris/Elab/Implementation.idr

@@ -228,6 +228,10 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
                -- 6. Add transnformation rules for top level methods
                traverse (addTransform impName upds) (methods cdata)
 
+               -- inline flag has done its job, and outside the interface
+               -- it can hurt, so unset it now
+               unsetFlag fc impName TCInline
+
                -- Reset the open hints (remove the named implementation)
                setOpenHints hs
                pure ()) mbody