c5cb67c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix simple application

c5cb67cEdwin Brady13 years ago

src/Idris/AbsSyntax.hs+2−2

@@ -1554,9 +1554,9 @@ stripLinear i tm = evalState (sl tm) [] where

1554 return (PPatvar fc f)

1555 sl t@(PAlternative _ (a : as)) = do sl a

1556 return t

1557− sl (PApp fc fn args) = do fn' <- sl fn

1557+ sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var

1558 args' <- mapM slA args

1559− return $ PApp fc fn' args'

1559+ return $ PApp fc fn args'

1560 where slA (PImp p m l n t) = do t' <- sl t

1561 return $ PImp p m l n t'

1562 slA (PExp p l t) = do t' <- sl t

src/Idris/Core/Elaborate.hs+4−4

@@ -611,10 +611,10 @@ simple_app fun arg appstr =

611 hs <- get_holes

612 env <- get_env

613 -- We don't need a and b in the hole queue any more since they were

614− -- just for checking f, so discard them if they are still there.

614+ -- just for checking f, so move them to the end. If they never end up

615− -- If they haven't been solved, regret will fail

615+ -- getting solved, we'll get an 'Incomplete term' error.

616− when (a `elem` hs) $ do focus a; regretWith (CantInferType appstr)

616+ when (a `elem` hs) $ do movelast a

617− when (b `elem` hs) $ do focus b; regretWith (CantInferType appstr)

617+ when (b `elem` hs) $ do movelast b

618 end_unify

619 where regretWith err = try regret

620 (lift $ tfail err)