git.iko.soy/Idris-dev
on master help sign in
Fix parameter propagation error
957dd61Edwin Brady
src/Idris/Elab/Utils.hs+3
compare with master
unifiedsplit
@@ -157,6 +157,9 @@ pvars ist _ = []
157getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi t _) sc)
157getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi t _) sc)
158 = nub $ getFixedInType i env [] t ++
158 = nub $ getFixedInType i env [] t ++
159 getFixedInType i (n : env) is (instantiate (P Bound n t) sc)
159 getFixedInType i (n : env) is (instantiate (P Bound n t) sc)
160+ ++ case t of
161+ P _ n _ -> if n `elem` env then [n] else []
162+ _ -> []
160getFixedInType i env (_ : is) (Bind n (Pi t _) sc)
163getFixedInType i env (_ : is) (Bind n (Pi t _) sc)
161 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)
164 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)
162getFixedInType i env is tm@(App f a)
165getFixedInType i env is tm@(App f a)