32c2467 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Account for 'let' with unbound implicits

Previously a 'let' in a type would be ignored for unbound implicits, leading to strange behaviour when the name bound in the let would get bound as an implicit argument too.

commit32c2467d4e5de37368efc727bd84f14db6ccbe08 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 11 Dec 2016, 23:10 (10 years ago) parent2196023

1 file changed+2

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+2

src/Idris/AbsSyntaxTree.hs+2

@@ -2472,6 +2472,8 @@ implicitNamesIn uvars ist tm

24722472 ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]

24732473 ni 0 env (PLam fc n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc

24742474 ni 0 env (PPi p n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc

2475+ ni 0 env (PLet fc n _ ty val sc) = do ni 0 env ty;

2476+ ni 0 env val; ni 0 (n:env) sc

24752477 ni 0 env (PRewrite _ _ l r _) = do ni 0 env l; ni 0 env r

24762478 ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r

24772479 ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r