1a1176d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Need to evaluate when finding linear args

A pattern may tell us more about whether an argument is linear or not

commit1a1176d629085810fbbe2434777c7d827e08e4cd authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 19 Dec 2016, 10:14 (10 years ago) parentfb185aa

1 file changed+2−1

unifiedsplit

src/Idris/Elab/Utils.hs+2−1

@@ -584,7 +584,8 @@ findLinear ist env tm | (P _ f _, args) <- unApply tm,

584584 findLinArg (Bind n (Pi c _ _ _) sc) (P _ a _ : as)

585585 | Rig0 <- c = (a, c) : findLinArg sc as

586586 | Rig1 <- c = (a, c) : findLinArg sc as

587− findLinArg (Bind n (Pi _ _ _ _) sc) (a : as) = findLinArg sc as

587+ findLinArg (Bind n (Pi _ _ _ _) sc) (a : as)

588+ = findLinArg (whnf (tt_ctxt ist) [] (substV a sc)) as

588589 findLinArg _ _ = []

589590findLinear ist env (App _ f a)

590591 = nub $ findLinear ist env f ++ findLinear ist env a