c5cb67c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix simple application

Don't expect the types to be inferred immediately. If the types of the arguments are not solved immediately, push their holes to the end of the hole queue rather than failing with a Can't Infer Type error. Also fix for linear patterns - don't erase a repeated name in a function application.

commitc5cb67cdfa5163c6e1fd5cc115aa9d13addf162c authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 21 Mar 2014, 11:02 (13 years ago) parent45a0add

2 files changed+6−6

compare with master

unifiedsplit

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

src/Idris/AbsSyntax.hs+2−2

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

15541554 return (PPatvar fc f)

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

15561556 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

15581558 args' <- mapM slA args

1559− return $ PApp fc fn' args'

1559+ return $ PApp fc fn args'

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

15611561 return $ PImp p m l n t'

15621562 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 =

611611 hs <- get_holes

612612 env <- get_env

613613 -- 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.

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

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

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

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

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

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

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

618618 end_unify

619619 where regretWith err = try regret

620620 (lift $ tfail err)