on master help sign in
Fix error in spotting linear arguments
0791659Edwin Brady
src/Idris/AbsSyntax.hs+5−2
@@ -1770,9 +1770,12 @@ stripLinear i tm = evalState (sl tm) [] where
1770 t' <- sl t
1770 t' <- sl t
1771 r' <- sl r
1771 r' <- sl r
1772 return (PDPair fc p l' t' r')
1772 return (PDPair fc p l' t' r')
1773+ sl (PApp fc fn args) = do fn' <- case fn of
1773− sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var
1774+ -- Just the args, fn isn't matchable as a var
1775+ PRef _ _ -> return fn
1776+ t -> sl t
1774 args' <- mapM slA args
1777 args' <- mapM slA args
1775− return $ PApp fc fn args'
1778+ return $ PApp fc fn' args'
1776 where slA (PImp p m l n t) = do t' <- sl t
1779 where slA (PImp p m l n t) = do t' <- sl t
1777 return $ PImp p m l n t'
1780 return $ PImp p m l n t'
1778 slA (PExp p l n t) = do t' <- sl t
1781 slA (PExp p l n t) = do t' <- sl t